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)

Full work available at URL https://doi.org/10.1016/0304-3975(92)90037-G

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

• 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
• 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?)
• 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

(22)

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

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)