Modules in Coq Are and Will Be Correct
Author:
- 1 January 2004
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 130-146
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Termination of rewriting in the Calculus of ConstructionsJournal of Functional Programming, 2003
- Implementing Modules in the Coq SystemLecture Notes in Computer Science, 2003
- A module system for a programming language based on the LF logical frameworkJournal of Logic and Computation, 1998
- A module calculus for pure type systemsLecture Notes in Computer Science, 1997
- A type-theoretic approach to higher-order modules with sharing1994
- Manifest types, modules, and separate compilation1994
- The calculus of constructionsInformation and Computation, 1988