Dependent Types at Work

DOI10.1007/978-3-642-03153-3_2zbMath1250.68086OpenAlexW1511530761WikidataQ56387763 ScholiaQ56387763MaRDI QIDQ5191088

Ana Bove, Peter Dybjer

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

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

• Coq
• Haskell
• Nuprl
• Polyp
• Epigram
• Agda

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