Dependently Typed Programming in Agda

DOI10.1007/978-3-642-04652-0_5zbMath1263.68038MaRDI QIDQ3649136

Ulf Norell

Publication date: 3 December 2009

Published in: Advanced Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04652-0_5

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

Related Items

Quotienting the delay monad by weak bisimilarity, Proof-relevant π-calculus: a constructive account of concurrency and causality, Unnamed Item, COCHIS: Stable and coherent implicits, Higher order functions and Brouwer’s thesis, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, A greedy algorithm for dropping digits, Partiality and Container Monads, POPLMark reloaded: Mechanizing proofs by logical relations, Heterogeneous binary random-access lists, Implementing type theory in higher order constraint logic programming, A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading, Finiteness and rational sequences, constructively, Unnamed Item, Unnamed Item, A correct-by-construction conversion from lambda calculus to combinatory logic, Naïve Type Theory, Admissible ordering on monomials is well-founded: a constructive proof, Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic, Agda, J-Calc: a typed lambda calculus for intuitionistic justification logic, A constructive manifestation of the Kleene-Kreisel continuous functionals, Formalizing semantic bidirectionalization and extensions with dependent types, Certified CYK parsing of context-free languages, Coalgebras in functional programming and type theory, Genetic programming \(+\) proof search \(=\) automatic improvement, Incorporating quotation and evaluation into Church's type theory, A certified program for the Karatsuba method to multiply polynomials, On a machine-checked proof for fraction arithmetic over a GCD domain, Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types, Formalizing constructive projective geometry in Agda, A web-based toolkit for mathematical word processing applications with semantics, Formalizing mathematical knowledge as a biform theory graph: a case study, A henkin-style completeness proof for the modal logic S5, A Classical Realizability Model for a Semantical Value Restriction, Type Theory Should Eat Itself, Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics, Auto in Agda, Program Calculation in Coq, Bisimulations Generated from Corecursive Equations, A Brief Overview of Agda – A Functional Language with Dependent Types, Unnamed Item, Galois Connections for Recursive Types, Synthesis of Recursive ADT Transformations from Reusable Templates, The Lean Theorem Prover (System Description)

Cites Work

• The view from the left
• The power of Pi