Program development in constructive type theory

DOI10.1016/0304-3975(92)90037-GMaRDI QIDQ1190474zbMATH OpenFDO

Authors Didier Galmiche

Publication date 26 September 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

program derivation from proofsprogramming with proofs

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Recommendations

• scientific article; zbMATH DE number 4147469
• scientific article; zbMATH DE number 177798
• Verifying programs in the calculus of inductive constructions
• Constructive system for automatic program synthesis
• scientific article; zbMATH DE number 140006

Cites work

• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 4148081 (Why is no real title available?)
• scientific article; zbMATH DE number 3827194 (Why is no real title available?)
• scientific article; zbMATH DE number 3907752 (Why is no real title available?)
• A set constructor for inductive sets in Martin-Löf's type theory
• A synthesis of several sorting algorithms
• Constructing recursion operators in intuitionistic type theory
• Constructive mathematics and computer programming
• Terminating general recursion
• The calculus of constructions
• The foundation of a generic theorem prover
• The system \({\mathcal F}\) of variable types, fifteen years later

Cited in

(19)

• Programming inductive proofs. A new approach based on contextual types
• scientific article; zbMATH DE number 4047195 (Why is no real title available?)
• Program development by proof transformation.
• scientific article; zbMATH DE number 4148081 (Why is no real title available?)
• Proof-search in type-theoretic languages: An introduction
• Constructive system for automatic program synthesis
• scientific article; zbMATH DE number 4143955 (Why is no real title available?)
• scientific article; zbMATH DE number 4133471 (Why is no real title available?)
• scientific article; zbMATH DE number 3952752 (Why is no real title available?)
• scientific article; zbMATH DE number 3907752 (Why is no real title available?)
• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• Combining programming with theorem proving
• Program derivation in type theory: A partitioning problem
• scientific article; zbMATH DE number 785043 (Why is no real title available?)
• A logical framework to model software development by multiple agents following a common specification
• On proof normalization in linear logic
• scientific article; zbMATH DE number 140006 (Why is no real title available?)
• From OBJ to ML to Coq
• scientific article; zbMATH DE number 177798 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl
• Automath

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)