A Brief Overview of Agda – A Functional Language with Dependent Types
From MaRDI portal
Publication:3183520
DOI10.1007/978-3-642-03359-9_6zbMath1252.68062MaRDI 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
68N18: Functional programming and lambda calculus
Related Items
Unnamed Item, Validating Brouwer's continuity principle for numbers using named exceptions, Unnamed Item, Unnamed Item, Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code, Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi, Characteristics of de Bruijn’s early proof checker Automath, Normalization by Evaluation for Typed Weak lambda-Reduction, How Hard Is Positive Quantification?, Containers, monads and induction recursion, A light-weight integration of automated and interactive theorem proving, On the Mints Hierarchy in First-Order Intuitionistic Logic, Formalising Mathematics in Simple Type Theory, Is Impredicativity Implicitly Implicit, Intuitionistic completeness of first-order logic, Recycling proof patterns in Coq: case studies, Flag-based big-step semantics, Coalgebras in functional programming and type theory, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Hammer for Coq: automation for dependent type theory, From types to sets by local type definition in higher-order logic, A consistent foundation for Isabelle/HOL, Type-specialized staged programming with process separation, Machine learning guidance for connection tableaux, Integrating induction and coinduction via closure operators and proof cycles, The effects of effects on constructivism, Functions-as-constructors higher-order unification: extended pattern unification, 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, Mechanized metatheory revisited, Formalization of universal algebra in Agda, An implementation of effective homotopy of fibrations, Congruence Closure in Intensional Type Theory, Exercising Nuprl’s Open-Endedness, From Types to Sets by Local Type Definitions in Higher-Order Logic, Modular Dependent Induction in Coq, Mendler-Style, A Consistent Foundation for Isabelle/HOL, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Friends with Benefits, Bisimulations Generated from Corecursive Equations, Extracting a DPLL Algorithm
Uses Software
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
