Dependent Types at Work
From MaRDI portal
Publication:5191088
DOI10.1007/978-3-642-03153-3_2zbMath1250.68086OpenAlexW1511530761WikidataQ56387763 ScholiaQ56387763MaRDI QIDQ5191088
Publication date: 28 July 2009
Published in: Language Engineering and Rigorous Software Development (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03153-3_2
Related Items (7)
Continuity of Gödel's system T definable functionals via effectful forcing ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ A Brief Overview of Agda – A Functional Language with Dependent Types ⋮ Higher-order games with dependent types ⋮ Programming with ornaments ⋮ Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types ⋮ Infinite sets that Satisfy the Principle of Omniscience in any Variety of Constructive Mathematics
Uses Software
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- LCF considered as a programming language
- Inductive families
- MetaML and multi-stage programming with explicit annotations
- Indexed induction-recursion
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- A general formulation of simultaneous inductive-recursive definitions in type theory
- A new approach to generic functional programming
- Advanced Functional Programming
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
- Modelling general recursion in type theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Dependent Types at Work
