ATS/LF: A type system for constructing proofs as total functional programs

zbMATH Open1226.68026MaRDI QIDQ3086789FDOQ3086789

Authors: Hongwei Xi 

Publication date: 30 March 2011

Recommendations

• Frontiers of Combining Systems
• Combining programming with theorem proving
• scientific article; zbMATH DE number 559219
• Combining proofs and programs in a dependently typed language
• System ST toward a type system for extraction and proofs of programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (9)

• Singleton, union and intersection types for program extraction
• System ST toward a type system for extraction and proofs of programs
• Types for Proofs and Programs
• Attributive Types for Proof Erasure
• An expressive, scalable type theory for certified code
• Tutorial on Subtype Marks
• Frontiers of Combining Systems
• Combining programming with theorem proving
• Combining proofs and programs in a dependently typed language

This page was built for publication: ATS/LF: A type system for constructing proofs as total functional programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3086789)