Proof-Assistants Using Dependent Type Systems
- 1 January 2001
- book chapter
- Published by Elsevier
- p. 1149-1238
- https://doi.org/10.1016/b978-044450813-3/50020-5
Abstract
No abstract availableThis publication has 14 references indexed in Scilit:
- Formal and Efficient Primality Proofs by Use of Computer Algebra OraclesJournal of Symbolic Computation, 2001
- Domain-free pure type systemsJournal of Functional Programming, 2000
- Coercive subtypingJournal of Logic and Computation, 1999
- The Impact of the Lambda Calculus in Logic and Computer ScienceBulletin of Symbolic Logic, 1997
- Synthesis of ML programs in the system CoqJournal of Symbolic Computation, 1993
- A framework for defining logicsJournal of the ACM, 1993
- Modular proof of strong normalization for the calculus of constructionsJournal of Functional Programming, 1991
- The calculus of constructionsInformation and Computation, 1988
- Computer programs for checking mathematical proofsProceedings of Symposia in Pure Mathematics, 1962
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940