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

MaRDI QIDQ3086789zbMATH OpenFDO

Authors Hongwei Xi

Publication date 30 March 2011

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)

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

Cited in

(9)

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

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)