Catálogo de publicaciones - libros

We present a tool for automated theorem proving in Agda, an implementation of Martin-Löf’s intuitionistic type theory. The tool is intended to facilitate interactive proving by relieving the user from filling in simple but tedious parts of a proof. The proof search is conducted directly in type theory and produces proof terms. Any proof term is verified by the Agda type-checker, which ensures soundness of the tool. Some effort has been spent on trying to produce human readable results, which allows the user to examine the generated proofs. We have tested the tool on examples mainly in the area of (functional) program verification. Most examples we have considered contain induction, and some contain generalisation. The contribution of this work outside the Agda community is to extend the experience of automated proof for intuitionistic type theory.

Surreal Numbers form a totally ordered (commutative) Field, containing copies of the reals and (all) the ordinals. I have encoded most of the Ring structure of surreal numbers in Coq. This encoding relies on Aczel’s encoding of set theory in type theory.

This paper discusses in particular the definitional or proving points where I had to diverge from Conway’s or the most natural way, like separation of simultaneous induction-recursion into two inductions, transforming the definition of the order into a mutually inductive definition of “at most” and “at least” and fitting the rather complicated induction/recursion schemes into the type theory of Coq.

We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions follow a two-level approach—they require less work than the standard techniques which inspired them [11,8]. Moreover, given a suitably heterogeneous notion of equality, they extend without difficulty to inductive families of datatypes. These constructions are vital components of the translation from dependently typed programs in pattern matching style [7] to the equivalent programs expressed in terms of induction principles [21] and as such play a crucial behind-the-scenes rôle in Epigram [25].

Within a framework of correct code-generation from HOL-specifications, we present a particular instance concerned with the optimized compilation of a lazy language (called MiniHaskell) to a strict language (called MiniML).

Both languages are defined as shallow embeddings into denotational semantics based on Scott’s cpo’s, leading to a derivation of the corresponding operational semantics in order to cross-check the basic definitions.

On this basis, translation rules from one language to the other were formally derived in Isabelle/HOL. Particular emphasis is put on the optimized compilation of function applications leading to the side-calculi inferring e.g. strictness of functions.

The derived rules were grouped and set-up as an instance of our generic, tactic-based translator for specifications to code.

Peter Hancock and Anton Setzer developed the notion of interface to introduce interactive programming into dependent type theory. We generalise their notion and get an even simpler definition for interfaces. With this definition the relationship of interfaces to games becomes apparent. In fact from a game theoretical point of view interfaces are nothing other than special games. Programs are strategies for these games. There is an obvious notion of refinement which coincides exactly with the intuition. Interfaces together with the re.nement relation build a complete lattice. We can define several operators on interfaces: tensor, par, choice, bang etc. Every notion has a dual notion by interchanging the viewpoint of player and opponent. Identifying strategies by some kind of behavioural equivalence we conjecture to receive a linear category. All results so far can be achieved in intensional Martin-Löf Type Theory and are verified in the theorem prover Agda (with the exception of associativity of composition which is only proved on paper until now).

We introduce a pure type system (PTS) λ with four sorts and show that this PTS captures the proof-theoretic strength of Zermelo’s set theory. For that, we show that the embedding of the language of set theory into λ via the ‘sets as pointed graphs’ translation makes λ a conservative extension of IZ+AFA+TC (intuitionistic Zermelo’s set theory plus Aczel’s antifoundation axiom plus the axiom of transitive closure)—a theory which is equiconsistent to Zermelo’s. The proof of conservativity is achieved by defining a retraction from λ to a (skolemised version of) Zermelo’s set theory and by showing that both transformations commute via the axioms AFA and TC.

In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic decision procedure for Epigram’s in-built equality at each type, taking a complementary approach to that of Benke, Dybjer and Jansson [7]. We also give a generic definition of map, taking our inspiration from Jansson and Jeuring [21]. Finally, we equip the regular universe with the partial derivative which can be interpreted functionally as Huet’s notion of ‘zipper’, as suggested by McBride in [27] and implemented (without the fixpoint case) in Generic Haskell by Hinze, Jeuring and Löh [18]. We aim to show through these examples that generic programming can be ordinary programming in a dependently typed language.

Baaz and Fermueller gave in 2003 an original characterization of constructive existence in classical logic [2]. In this note, we give a simple proof of this result based on cut-elimination in sequent calculus. The interest of this proof besides its simplicity is that it allows in particular to generalize the result to other logics enjoying cut-elimination. We also briefly discuss the significance of the characterization itself.