Constructive Membership Predicates as Index Types
From MaRDI portal
Publication:2866329
DOI10.1016/j.entcs.2006.10.034zbMath1277.68054OpenAlexW2040832496MaRDI QIDQ2866329
Publication date: 13 December 2013
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2006.10.034
constructive type theoryrecursive typesindexesCurry-HowardNuprlproofs-as-programsmembership predicates
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Search algorithms in type theory
- A semantics for shape
- Containers: Constructing strictly positive types
- Combining programming with theorem proving
- Isomorphisms of generic recursive polynomial types
- Building reliable, high-performance networks with the Nuprl proof development system
- The view from the left
- The marriage of effects and monads
- Cayenne—a language with dependent types
- Types for Proofs and Programs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Constructive Membership Predicates as Index Types