References

[1] Peter Aczel and David P. Carlisle. The logical theory of constructions: A formal framework and its implementation. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 19–38, May 1990.

In this report we describe the implementation of a version of the LTC (Logical Theory of Constructions) framework in the Generic Theorem Prover Isabelle. An earlier version of the framework was described by Aczel and Mendler in [24].

[2] Lennart Augustsson, Thierry Coquand, and Bengt Nordström. A short description of another logical framework. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 39–42, May 1990.

This note is an incomplete description of an incomplete implementation of another logical framework.

[3] David Basin and Matt Kaufmann. The Boyer-Moore prover and Nuprl: An experimental comparison. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 43–65, May 1990.

We use an example to compare the Boyer-Moore Theorem Prover and the Nuprl Proof Development System. The respective machine verifications of a version of Ramsey’s theorem illustrate similarities and differences between the two systems. The proofs are compared using both quantitative and non-quantitative measures, and we examine difficulties in making such comparisons.

[4] Stefano Berardi. Girard normalization proof in LEGO. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 67–77, May 1990.

This paper is a report of the first attempt, in part successful, to formalize in LEGO (a mechanical proof-checker based on Pure Construction Calculus PCC) a large and difficult proof: Girard’s proof of strong normalization for second order lambda calculus. We describe in an informal and general way the problems we had to face, since we believe that most of them are common to all proof-checkers implemented up to now.

[5] Alan Bundy, Alan Smaill, and Jane Hesketh. Turning eureka steps into calculations in automatic program synthesis. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 79–87, May 1990.

We describe a technique called middle-out reasoning for the control of search in automatic theorem proving. We illustrate its use in the domain of automatic program synthesis. Programs can be synthesised from proofs that their logical specifications are satisfiable. Each proof step is also a program construction step. Unfortunately, a naive use of this technique requires a human or computer to produce proof steps which provide the essential structure of the desired program. It is hard to see the justification for these steps at the time that they are made; the reason for them emerges only later in the proof. Such proof steps are often call ‘eureka’ steps. Middle-out reasoning enables these eureka steps to be produced, automatically, as a side effect of non-eureka steps.

[6] Rod Burstall and Furio Honsell. A natural deduction treatment of operational semantics. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 89–111, May 1990.

We show how Natural Deduction extended with two replacement operators can provide a framework for defining programming languages, a framework which is more expressive than the usual Operational Semantics presentation in that it permits hypothetical premises. This allows us to do without an explicit environment and store. Instead we use the hypothetical premises to make assumptions about the values of variables. We define the extended Natural Deduction logic using the Edinburgh Logical Framework.

[7] Rod Burstall and James McKinna. Deliverables: an approach to program development in the calculus of constructions. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 113–121, May 1990.

[8] Martin Coen. Interactive program synthesis within ZF set theory. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 463–477, May 1990.

Program synthesis may be regarded as a theorem proving task. The program to be synthesized is a “logical variable” which is instantiated during the proof of its specification. An attempt to produce a theory for program synthesis is described, by defining a simple programming language of total functions within ZF set theory. The resulting framework allows reasoning about programs using well-founded recursion and induction, and has been used to derive a unification algorithm. The theory has been implemented on machine using Paulson’s theorem prover Isabelle.

[9] Robert L. Constable and Chet Murthy. Finding computational content in classical proofs. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 141–156, May 1990.

We illustrate the effectiveness of proof transformations which bring out the computational content of classical proofs even in cases where it is not apparent. We state without proof a theorem that these transformations apply to proofs in a fragment of type theory and discuss the implementation of these in Nuprl. We end with a discussion of the revealing applications to Higman’s lemma by the second author using the implemented system.

[10] Thierry Coquand. An algorithm for testing conversion in type theory (preliminary version). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 157–166, May 1990.

We prove the correctness and completeness of an algorithm for testing conversion in type theory. The method applies to Edinburgh LF.

[11] Thierry Coquand and Jean Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 479–497, May 1990.

We give a proof that all terms that type-check in the theory of contructions are strongly normalizing (under β-reduction). The main novelty of this proof is that it uses a “Kripke-like” interpretation of the types and kinds, and that it does not use infinite contexts. We explore some consequences of strong normalization, consistency and decidability of type-checking. We also show that our proof yields another proof of strong normalization for LF (under β-reduction), using the reducibility method.

[12] N. G. de Bruijn. A plea for weaker frameworks. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 123–140, May 1990.

It is to be expected that logical frameworks will become more and more important in the near future, since they can set the stage for an integrated treatment of verification systems for large areas of the mathematical sciences (which may contain logic, mathematics, and mathematical constructions in general, such as computer software and computer hardware). It seems that the moment has come to try to get to some kind of a unification of the various systems that have been proposed.

Over the years there has been the tendency to strengthen the frameworks by rules that enrich the notion of definitional equality, thus causing impurities in the backbones of those frameworks: the typed lambda calculi. In this paper a plea is made for going into the opposite direction: expel those impurities from the framework to the books, where the role of definitional equality is taken over by (possibly strong) book equality.

[13] Philippe de Groote. Nederpelt’s calculus extended with a notion of context as a logical framework. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 167–179, May 1990.

We define an extended version of Nederpelt’s calculus which can be used as a logical framework. The extensions have been introduced in order to support the notions of mathematical definition of constants and to internalize the notion of theory. The resulting calculus remains concise and simple, a basic requirement for logical frameworks. The calculus manipulates two kind of objects: texts which correspond to λ-expressions, and contexts which are mainly sequences of variable declarations, constant definitions, or context abbreviations. Basic operations on texts and contexts are provided. It is argued that these operations allow one to structure large theories. An example is provided.

[14] Joëlle Despeyroux. Theo, an interactive proof development system (abstract). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), page 181, May 1990.

[15] Gilles Dowek. A proof synthesis algorithm for a mathematical vernacular (draft). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 183–212, May 1990.

A Mathematical Vernacular is a language in which mathematics can be written, both usable for publishing and mathematically fully described. We present a step toward such a language that uses the Calculus of Constructions as a foundation.

The main idea is to get rid of proof-terms and write demonstrations of theorems as sequences of propositions, in such a way that a proof of each proposition is obvious when previous propositions are known. A proof-synthesis system is developed in order to check that a sequence of propositions is indeed a demonstration.

[16] Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 213–229, May 1990.

Martin-Löf’s type theory is presented in several steps. The kernel is a dependently typed λ-calculus. Then there are schemata for inductive sets and families of sets and for primitive recursive functions and families of functions. Finally, there are set formers (generic polymorphism) and universes. At each step syntax, inference rules, and set-theoretic semantics are given.

[17] Amy Felty and Dale Miller. Encoding a dependent-type λ-calculus in a logic programming language. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 231–244, May 1990.

Various forms of typed λ-calculi have been proposed as specification languages for representing wide varieties of object logics. The logical framework, LF, is an example of such a dependenttype λ-calculus. A small subset of intuitionistic logic with quantification over simply typed λ-calculus has also been proposed as a framework for specifying general logics. The logic of hereditary Harrop formulas with quantification at all non-predicate types, denoted here as hh^{ω}, is such a meta-logic that has been implemented in both the Isabelle theorem prover and the λProlog logic programming language. Both frameworks provide for specifications of logics in which details involved with free and bound variable occurrences, substitutions, eigenvariables, and the scope of assumptions within object logics are handled correctly and elegantly at the “meta” level. In this paper, we show how LF can be encoded into hh^{ω} in a direct and natural way by mapping the typing judgments in LF into propositions in the logic of hh^{ω}. This translation establishes a very strong connection between these two languages: the order of quantification in an LF signature is exactly the order of a set of hh^{ω} clauses, and the proofs in one system correspond directly to proofs in the other system. Relating these two languages makes it possible to provide implementations of proof checkers and theorem provers for logics specified in LF by using standard logic programming techniques which can be used to implement hh^{ω}.

[18] Jean-Yves Girard. Logic vs logics: A methodological panel. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 245–246, May 1990.

[19] Lars Hallnäs. Models of partial inductive definitions. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 247–257, May 1990.

[20] Leen Helmink and René Ahn. Goal directed proof construction in type theory. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 259– 297, May 1990.

In this paper, a method is presented for proof construction in Generalised Type Systems. An interactive system that implements the method has been developed.

[21] Matt Kaufmann. Demo of the Boyer-Moore theorem prover and some of its extensions. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 299–322, May 1990.

[22] Nax Paul Mendler. Quotient types via coequalizers in Martin-Löf type theory. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 349– 360, May 1990.

This note describes the notion of quotient type as it arises from coequalizers in a category of types, as an exercise in working from a categorical property to arrive at its expression in the type theory. As examples, we use quotient types to internalize the notion of being an epic morphism, and to define “squash” types, and with squash types, a weak version of the subset type constructor. Some familiarity with the semantics of Martin-Löf type theory is assumed, but we’ll begin with an overview. …

[23] Nax Paul Mendler. A series of type theories and their interpretations in the logical theory of constructions. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 337–348, May 1990.

We present three Martin-Löf type theories in a natural deduction style: T T_{0}, a type theory without a type universe; T T_{1}, a type theory with one type universe; and T T_{ω}, a type theory with a cumulative hierarchy of type universes. Then we give interpretations of each in a corresponding LTC theory.

[24] Paul F. Mendler and Peter Aczel. The notion of a Framework and a framework for LTC. In Third Annual Symposium on Logic in Computer Science, pages 392–399. IEEE, 1988.

[25] Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 323–335, May 1990.

Most conventional programming languages have direct methods for representing first-order terms (say, via concrete datatypes in ML). If it is necessary to represent structures containing bound variables, such as λ-terms, formulas, types, or proofs, these must first be mapped into first-order terms, and then a significant number of auxiliary procedures must be implemented to manage bound variable names, check for free occurrences, do substitution, test for equality modulo alpha-conversion, etc. We shall show how the applicative core of the ML programming language can be enhanced so that λ-terms can be represented more directly and so that the enhanced language, called ML_{λ}, provides a more elegant method of manipulating bound variables within data structures. In fact, the names of bound variables will not be accessible to the ML_{λ} programmer. This extension to ML involves the following: introduction of the new type constructor 'a => 'b for the type of λ-terms formed by abstracting a parameter of type 'a out of a term of type 'b; a very restricted and simple form of higher-order pattern matching; a method for extending a given data structure with a new constructor; and, a method for extending function definitions to handle such new constructors. We present several examples of ML_{λ} programs.

[26] Tobias Nipkow. A critical pair lemma for higher-order rewrite systems and its application to λ^{∗} (draft version). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 361–376, May 1990.

We consider rewrite systems over simply typed λ-terms where the left-hand sides obey the following restriction: in their β-normal form, any occurrence of a free variable x must be of the form x(y_{1},…, y_{n}), where the y_{i} are distinct bound variables. Calling such terms “patterns” we obtain two important results:

• Unification of two patterns is decidable and single most general unifiers exist. This result is due to Dale Miller.

• The critical pair lemma can be extended from first-order to such restricted higher-order

rewrite systems. This framework can be used to formalize the reduction relation in various typed λ-calculi and obtain confluence results by simple critical pair considerations. This is demonstrated for a particular system, λ^{∗}, which combines product and function types by imposing certain equalities between them, namely all the isomorphisms in a CCC, minus commutativity of products. A potential application of this system to the unification problem for the typed λ-calculus with ml-style polymorphism is sketched.

[27] Christine Paulin and Benjamin Werner. Extracting and executing programs developed in the inductive constructions system: a progress report. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 377–389, May 1990.

The experiment we describe here, consists in using program specifications proved in the Calculus of Constructions enhanced by inductive definitions, to extract their computational contents, and to execute them in a high-level functional language. We try to explain the need for a well-adapted target language to execute the mechanically extracted programs. In order to point out the related problems, we realized a first rudimentary implementation and we show the system working on an classical example.

[28] Frank Pfenning. Elf: A language for logic definition and verified metaprogramming (preliminary version). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 391–406, May 1990.

We describe Elf, a metalanguage for proof manipulation environments that are independent of any particular logical system. Elf is intended for meta-programs such as theorem provers, proof transformers, or type inference programs for programming languages with complex type systems. Elf unifies logic definition (in the style of LF, the Edinburgh Logical Framework) with logic programming (in the style of λProlog). It achieves this unification by giving types an operational interpretation, much the same way that Prolog gives certain formulas (Hornclauses) an operational interpretation. Novel features of Elf include: (1) the Elf search process automatically constructs terms that can represent object-logic proofs, and thus a program need not construct them explicitly, (2) the partial correctness of meta-programs with respect to a given logic can be expressed and proved in Elf itself, and (3) Elf exploits Elliott’s unification algorithm for a λ-calculus with dependent types.

[29] Colin Phillips. Implementing general recursion in type theory. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 407–419, May 1990.

This paper describes an implementation of Nordström’s acc type in Oyster, a version of the NUPRL system. Amongst the problems involved in using Martin-Löf’s type theory as a program language are those that arise because of computational redundancy and the lack of an adequate mechanism for dealing with general recursion. Bengt Nordström has proposed an extension to type theory — the Acc type — which provides a possible mechanism for dealing with these problems. This paper describes the mechanism for implementing the Acc type in Oyster. There is also a discussion of a number of examples including a derivation of the quicksort program and the lambo program.

[30] Randy Pollack. Implicit syntax (draft). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 421–433, May 1990.

A proof checking system may support syntax that is more convenient for users than its ‘official’ language. For example LEGO (a typechecker for several systems related to the Calculus of Constructions) has algorithms to infer some polymorphic instantiations (e.g. pair 2 true instead of pair nat bool 2 true) and universe levels (e.g. Type instead of Type(4)). Users need to understand such features, but do not want to know the algorithms for computing them. In this note I explain these two features by non-deterministic operational semantics for “translating” implicit syntax to the fully explicit underlying formal system. The translations are sound and complete for the underlying type theory, and the algorithms (which I will not talk about) are sound (not necessarily complete) for the translations. This note is phrased in terms of a general class of type theories. The technique described has more general application.

[31] David Pym and Lincoln Wallen. Investigations into proof-search in a system of first-order dependent function types. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 435–452, May 1990.

We present a series of proof systems for λΠ-calculus: a theory of first-order dependent function types. The systems are complete for the judgement of interest but differ substantially as bases for algorithmic proof-search. Each calculus in the series induces a search space that is properly contained within that of its predecessor. The λΠ-calculus is a candidate general logic in that it provides a metalanguage suitable for the encoding of logical systems and mathematics. Proof procedures formulated for the metalanguage extend to suitably encoded object logics, thus removing the need to develop procedures for each logic independently. This work is also an exploration of a systematic approach to the design of proof procedures. It is our contention that the task of designing a computationally efficient proof procedure for a given logic can be approached by formulating a series of calculi that possess specific proof-theoretic properties. These properties indicate that standard computational techniques such as unification are applicable, sometimes in novel ways. The study below is an application of this design method to an intuitionistic type theory.

Our methods exploit certain forms of subformula property and reduction ordering — a notion introduced by Bibel for classical logic, and extended by Wallen to various non-classical logics — to obtain a search calculus for which we are able to define notions of compatibility and intrinsic well-typing between a derivation ψ and a substitution σ calculated by unification which closes ψ (a derivation is closed when all of its leaves are axioms). Compatibility is an acyclicity test, a generalization of the occurs-check which, subject to intrinsic well-typing, determines whether the derivation ψ and substitution σ together constitute a proof.

Our work yields the (operational) foundations for a study of logic programming in this general setting. This potential is not explored here.

[32] Peter Schroeder-Heister. The role of elimination inferences in a structural framework (draft). In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks (Preliminary Proceedings), pages 453–462, May 1990.

It is claimed that introduction and elimination inferences operate at different levels. Whereas introduction inferences express logical rules in the genuine sense, elimination inferences are more like structural inferences. This is blurred by certain features of intuitionistic logic, but becomes obvious when systems with weaker structural postulates are considered.