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

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

• Coq
• 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