Dependent Types at Work

DOI10.1007/978-3-642-03153-3_2zbMath1250.68086WikidataQ56387763 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

68N18: Functional programming and lambda calculus

Related Items

Programming with ornaments, Continuity of Gödel's system T definable functionals via effectful forcing, A constructive manifestation of the Kleene-Kreisel continuous functionals, 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, A Brief Overview of Agda – A Functional Language with Dependent Types

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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