The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We propose a notion of pure type system with implicit coercions. In our framework, judgements are extended with a context of coercions Δ and the application rule is modified so as to allow coercions to be left implicit. The setting supports multiple inheritance and can be applied to all type theories with Π-types. One originality of our work is to propose a computational interpretation for implicit...
We present a simple and effective methodology for equational reasoning in proof checkers. The method is based on a two-level approach distinguishing between syntax and semantics of mathematical theories. The method is very general and can be carried out in any type system with inductive and oracle types. The potential of our two-level approach is illustrated by some examples developed in Lego.
This paper studies the problem of coherence in category theory from a type-theoretic viewpoint. We first show how a Curry-Howard interpretation of a formal proof of normalization for monoids almost directly yields a coherence proof for monoidal categories. Then we formalize this coherence proof in intensional intuitionistic type theory and show how it relies on explicit reasoning about proof objects...
The continuum is here presented as a formal space by means of a finitary inductive definition. In this setting a constructive proof of the Heine-Borel covering theorem is given.
An inductive definition of a set is often informally presented by giving some rules that explain how to build the elements of the set. The closure property states that any object is in the set if and only if it has been generated according to the formation rules. This is enough to justify case analysis reasoning: we can read the formation rules backwards to derive the necessary conditions for a given...
We present a simple notion of marking of first order formulas, which enables to optimize program extraction from intuitionistic Natural Deduction proofs. It gives a way to mark some parts of a proof depending on the marking of its conclusion. Thus it allows to remove useless code from the extracted λ-terms. We define a notion of realizability by which we prove the correctness of programs extracted...
We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to ordinary syntax and yet has a clean categorical description. We also present categories with families as a generalized algebraic theory. Then we define categories with families formally in Martin-Löf's intensional intuitionistic type theory. Finally, we discuss the coherence problem...
We describe an experience concerning the implementation and use of co-inductive types in the proof editor Coq. Co-inductive types are recursive types which, opposite to inductive ones, may be inhabited by infinite objects. In order to illustrate their use in Coq, we describe an axiomatisation of a calculus of broadcasting systems where non-ending processes are represented using infinite objects. This...
We investigate the relationship between intensional and extensional formulations of Martin-Löf type theory. We exhibit two principles which are not provable in the intensional formulation: uniqueness of identity and functional extensionality. We show that extensional type theory is conservative over the intensional one extended by these two principles, meaning that the same types are inhabited, whenever...
Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as LEGO, Coq, etc. In fact, ND-style systems are the kind of systems which can take best advantage of the possibility of reasoning “under assumptions” offered by proof assistants generated by Logical Frameworks. In...
A modular type/proof checking algorithm for incomplete proof objects is presented, where an incomplete proof object is represented as a term containing placeholders denoting the unfinished parts of the proof. The algorithm is designed for Martin-Löf 's type theory with explicit substitutions, but the general ideas can be adapted to similar theories. It is the kernel of the proof editor ALF. ...
We consider a simply typed λ-calculus with constants of ground types, and assume that for one ground type o, there are finitely many constants of type o. We call minimal model the quotient by observational equivalence of the set of all closed terms whose type is of terminal subformula o. We show that this model is decidable: all classes of any given type are recursively representable, and observational...
This paper presents the proof of correctness of a multiplier circuit formalized in the Calculus of Inductive Constructions. It uses a representation of the circuit as a function from the stream of inputs to the stream of outputs. We analyze the computational aspect of the impredicative encoding of coinductive types and show how it can be used to represent sequential circuits. We identify general proof...
We present a model construction for the Calculus of Constructions (CC) where all dependencies are carried out in a set-theoretical setting. The Soundness Theorem is proved and as a consequence of it Strong Normalization for CC is obtained. Some other applications of our model constructions are: showing that CC + Classical logic is consistent (by constructing a model for it) and showing that the Axiom...
The paper presents sound and complete translations of several fragments of Martin-Löf's monomorphic type theory to first order predicate calculus. The translations are optimised for the purpose of automated theorem proving in the mentioned fragments. The implementation of the theorem prover Gandalf and several experimental results are described.
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.