375 research outputs found
Bacteria in Paper - Hol Whitesides Dekker
No full textData repository for paper:
Title: Bacteria in Paper, a versatile platform to study bacterial ecology
Author(s): Hol, Felix; Whitesides, George; Dekker, Cees
Ecology Letters 2019</p
A Reference Version of HOL
No full text. The second author has implemented a reference version of the HOL logic (henceforth called gtt). This version, written in Standard ML, is as simple as possible, making as few assumptions as necessary to present the essence of HOL. This simplicity makes the implementation easy to understand, to port, to develop, to change, and to informally reason about. The first author has ported gtt to another dialect of ML, and developed the parsing, prettyprinting, and typechecking support needed to take gtt beyond its initial rudimentary conception. The implementation of gtt has already been of use in developing a variant of the HOL logic. As of this writing, there are at least four or five extant implementations of the HOL logic. These have been intensively developed, in some cases over decades, which leads us to an overwhelming question: why another? In particular, why gtt? There are several answers to this, stemming from different desires and needs in the HOL community. Changing the logic a ..
A New Interface for HOL - Ideas, Issues and Implementation
No full text. TkHolWorkbench is a new set of interface tools for HOL implemented using the Tk toolkit. It aims to be robust, extensible, lightweight and user-friendly. The tools are designed to augment the existing HOL interface. The project applies rapid prototyping and the use of an interpreted toolkit to the field of theorem proving interfaces. The topics considered in this paper are: the motivations for a new interface for HOL; the design objectives and usability targets for TkHolWorkbench; a description of the TkHolWorkbench tools as they now stand; and the extensible design architecture used in the implementation. 1 Introduction This paper describes a new interface for the HOL theorem proving system called TkHolWorkbench. This interface has been under development at the University of Cambridge for the last 6 months, and the author hopes that this interface, or some derivative of it, will eventually become the interface of the HOL2000 project. The aim of this paper is to give an overview of..
IMPLEMENTING TEMPORAL LOGIC IN HOL AND APPLICATIONS
No full textHigher-Order Logic (HOL) system has been proved to be very powerful for
hardware verification. Many of the largest proofs completed to date have
been constructed using HOL system. It seems to be that the HOL system is
more suitable for dealing with static object though we can define
functions with parameter of time for handling dynamic objects in HOL
system. On the other hand, Temporal logic which includes time in its
semantics has the potential of handling timing problems. In order to
mechanize the deducing process of temporal logic and explore the
possibilities of applying temporal logic to hardware verification, we
have tried to implement the linear timing temporal logic on the top
level of HOL system by expressing the temporal logic concepts in
high-order logic and proving the axioms and inference rules of a formal
temporal logic system. This paper describes the ideas and results of this
work, and gives some examples of applying temporal logic to hardware
specification and verification. We have proved that there exists a static
hazard in the combinational circuit considered under certain conditions,
and the hazard is eliminated in the improved circuit. We have also
specified and verified the properties of a S-R latch by the combined
power of temporal logic and HOL system.We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at [email protected]
Cut-elimination, substitution and normalisation
No full textDate of Acceptance: 01/2015We present a proof (of the main parts of which there is a formal version, checked with the Isabelle proof assistant) that, for a G3-style calculus covering all of intuitionistic zero-order logic, with an associated term calculus, and with a particular strongly normalising and confluent system of cut-reduction rules, every reduction step has, as its natural deduction translation, a sequence of zero or more reduction steps (detour reductions, permutation reductions or simplifications). This complements and (we believe) clarifies earlier work by (e.g.) Zucker and Pottinger on a question raised in 1971 by Kreisel.Peer reviewe
Interfacing Coq + SSReflect with GAP
No full textPresentation slides and preprint both provided by author. Preprint published in Electronic Notes in Theoretical Computer Science: Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10).We report on an extendable implementation of the communication interface connecting Coq proof assistant to the computational algebra system GAP using the Symbolic Computation Software Composability Protocol (SCSCP). It allows Coq to issue OpenMath requests to a local or remote GAP instances and represent server responses as Coq terms.Peer reviewe
Engraved portrait of John Bunyan, author (1628-1688)
No full textEngraved portrait of John Bunyan, author (1628-1688) drawn by Derby from an authentic portrait & engraved by W. Hol
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
No full textWe introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem proverOpen access funding provided by Chalmers University of Technology. The first and fifth authors were partly supported by the Swedish Foundation for Strategic Research. The seventh author was supported by an A*STAR National Science Scholarship (Ph.D.), Singapore. The third author was supported by the UK Research Institute in Verified Trustworthy Software Systems (VeTSS)
VERIFYING SECD IN HOL
No full textThis paper describes some of the work done at Calgary on
the design of an SECD chip and its verification using the Cambridge HOL proof
assistant. The chip is a physical realization of Henderson's variant
of Landin's abstract architecture to execute the lambda calculus. The
machine uses closures and includes explicit machine instructions to
assist recursion.
The complete proof, which goes from an abstract specification down to the
transistor level, is far too involved to be covered in a single paper. In
this paper, we discuss the SECD architecture and design and trace through
a portion of the proof of correctness of one sequence of the microcode.We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at [email protected]
A Definitional Encoding of TLA in Isabelle/HOL
No full textWe mechanise the logic TLA ∗ [8], an extension of Lamport’s Tem-poral Logic of Actions (TLA) [5] for specifying and reasoning about concurrent and reactive systems. Aiming at a framework for mechanis-ing the verification of TLA (or TLA∗) specifications, this contribution reuses some elements from a previous axiomatic encoding of TLA in Isabelle/HOL by the second author [7], which has been part of the Isabelle distribution. In contrast to that previous work, we give here a shallow, definitional embedding, with the following highlights: a theory of infinite sequences, including a formalisation of the concepts of stuttering invariance central to TLA and TLA*; a definition of the semantics of TLA*, which extends TLA by a mutually-recursive definition of formulas and pre-formulas, gen-eralising TLA action formulas; a substantial set of derived proof rules, including the TLA * ax
- …
