A Brief Overview of Agda – A Functional Language with Dependent Types

DOI10.1007/978-3-642-03359-9_6zbMath1252.68062OpenAlexW1558175043MaRDI QIDQ3183520

Ulf Norell, Peter Dybjer, Ana Bove

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_6

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (41)

How Hard Is Positive Quantification? ⋮ The effects of effects on constructivism ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Bisimulations Generated from Corecursive Equations ⋮ Extracting a DPLL Algorithm ⋮ Hammer for Coq: automation for dependent type theory ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Type-specialized staged programming with process separation ⋮ Intuitionistic completeness of first-order logic ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ Formalising Mathematics in Simple Type Theory ⋮ An implementation of effective homotopy of fibrations ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Coalgebras in functional programming and type theory ⋮ A relaxation of Üresin and Dubois' asynchronous fixed-point theory in Agda ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ Unnamed Item ⋮ From types to sets by local type definition in higher-order logic ⋮ Friends with Benefits ⋮ Unnamed Item ⋮ Recycling proof patterns in Coq: case studies ⋮ A consistent foundation for Isabelle/HOL ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Is Impredicativity Implicitly Implicit ⋮ Flag-based big-step semantics ⋮ Containers, monads and induction recursion ⋮ A light-weight integration of automated and interactive theorem proving ⋮ Machine learning guidance for connection tableaux ⋮ Unnamed Item ⋮ On the Mints Hierarchy in First-Order Intuitionistic Logic ⋮ Congruence Closure in Intensional Type Theory ⋮ Exercising Nuprl’s Open-Endedness ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Modular Dependent Induction in Coq, Mendler-Style ⋮ Mechanized metatheory revisited ⋮ Formalization of universal algebra in Agda ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi

Uses Software

• Unnamed Item
• Agda

Cites Work

• 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.
• The calculus of constructions
• Inductive families
• Indexed induction-recursion
• The Four Colour Theorem: Engineering of a Formal Proof
• Dependently Typed Programming in Agda
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Dependent Types at Work

This page was built for publication: A Brief Overview of Agda – A Functional Language with Dependent Types