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

zbMATH Open1226.68026MaRDI QIDQ3086789FDOQ3086789

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 (3)

• System ST toward a type system for extraction and proofs of programs
• Types for Proofs and Programs
• Attributive Types for Proof Erasure

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)