Frontiers of Combining Systems

DOI10.1007/11559306MaRDI QIDQ5491909zbMATH OpenOpenAlexFDO

Authors Sa Cui, Kevin Donnelly, Hongwei Xi

Publication date 10 October 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11559306

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• ATS/LF: A type system for constructing proofs as total functional programs
• Combining programming with theorem proving
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Combining proofs and programs in a dependently typed language
• Dependently Typed Programming Based on Automated Theorem Proving

Cited in

(5)

• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Attributive Types for Proof Erasure
• Combining programming with theorem proving
• ATS/LF: A type system for constructing proofs as total functional programs
• Combining proofs and programs in a dependently typed language

Describes a project that uses

Uses Software

• Automath
• Nuprl

This page was built for publication: Frontiers of Combining Systems

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