Frontiers of Combining Systems
From MaRDI portal
Publication:5491909
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
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)