Program development in constructive type theory
From MaRDI portal
Publication:1190474
DOI10.1016/0304-3975(92)90037-GzbMATH Open0760.68012MaRDI QIDQ1190474FDOQ1190474
Authors: Didier Galmiche 
Publication date: 26 September 1992
Published in: Theoretical Computer Science (Search for Journal in Brave)
Recommendations
Cites Work
- The system \({\mathcal F}\) of variable types, fifteen years later
- The calculus of constructions
- A synthesis of several sorting algorithms
- Title not available (Why is that?)
- Terminating general recursion
- Constructing recursion operators in intuitionistic type theory
- Title not available (Why is that?)
- The foundation of a generic theorem prover
- Constructive mathematics and computer programming
- A set constructor for inductive sets in Martin-Löf's type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (19)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- On proof normalization in linear logic
- Title not available (Why is that?)
- Programming inductive proofs. A new approach based on contextual types
- A logical framework to model software development by multiple agents following a common specification
- Constructive system for automatic program synthesis
- Title not available (Why is that?)
- Program derivation in type theory: A partitioning problem
- From OBJ to ML to Coq
- Title not available (Why is that?)
- Combining programming with theorem proving
- Program development by proof transformation.
- Proof-search in type-theoretic languages: An introduction
- Title not available (Why is that?)
- Title not available (Why is that?)
Uses Software
This page was built for publication: Program development in constructive type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1190474)
