Dependently Typed Programming in Agda

DOI10.1007/978-3-642-04652-0_5zbMath1263.68038OpenAlexW4242767025MaRDI 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

Functional programming and lambda calculus (68N18)

Related Items (45)

J-Calc: a typed lambda calculus for intuitionistic justification logic ⋮ A web-based toolkit for mathematical word processing applications with semantics ⋮ Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ A certified program for the Karatsuba method to multiply polynomials ⋮ The Lean Theorem Prover (System Description) ⋮ Partiality and Container Monads ⋮ Bisimulations Generated from Corecursive Equations ⋮ A Brief Overview of Agda – A Functional Language with Dependent Types ⋮ Quotienting the delay monad by weak bisimilarity ⋮ Formalizing semantic bidirectionalization and extensions with dependent types ⋮ Auto in Agda ⋮ 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 ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Heterogeneous binary random-access lists ⋮ A henkin-style completeness proof for the modal logic S5 ⋮ Coalgebras in functional programming and type theory ⋮ Unnamed Item ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Finiteness and rational sequences, constructively ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On a machine-checked proof for fraction arithmetic over a GCD domain ⋮ Certified CYK parsing of context-free languages ⋮ Galois Connections for Recursive Types ⋮ Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types ⋮ Synthesis of Recursive ADT Transformations from Reusable Templates ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Genetic programming \(+\) proof search \(=\) automatic improvement ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Program Calculation in Coq ⋮ 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 ⋮ COCHIS: Stable and coherent implicits ⋮ Agda ⋮ Implementing type theory in higher order constraint logic programming ⋮ Formalizing constructive projective geometry in Agda ⋮ 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

Cites Work

• The view from the left
• The power of Pi

This page was built for publication: Dependently Typed Programming in Agda