Dependently typed programming in Agda

DOI10.1007/978-3-642-04652-0_5MaRDI QIDQ3649136zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A Brief Overview of Agda – A Functional Language with Dependent Types
• Dependent Types at Work
• scientific article; zbMATH DE number 2090721
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Generic programming with dependent types

Cites work

• The power of Pi
• The view from the left

Cited in

(69)

• Incorporating quotation and evaluation into Church's type theory
• A certified program for the Karatsuba method to multiply polynomials
• Agda
• 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
• J-Calc: a typed lambda calculus for intuitionistic justification logic
• 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
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Auto in Agda. Programming proof search using reflection
• A tutorial implementation of a dependently typed lambda calculus
• Program calculation in Coq
• Bisimulations generated from corecursive equations
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Galois Connections for Recursive Types
• Synthesis of recursive ADT transformations from reusable templates
• Everybody's got to be somewhere
• The Lean theorem prover (system description)
• Formalizing semantic bidirectionalization and extensions with dependent types
• : dependent types without the sugar
• Do we need dependent types?
• Quotienting the delay monad by weak bisimilarity
• Generic programming with dependent types
• Certified CYK parsing of context-free languages
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• scientific article; zbMATH DE number 2090721 (Why is no real title available?)
• Dependently-typed formalisation of typed term graphs
• COCHIS: stable and coherent implicits
• Variations on Noetherianness
• 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
• Security-typed programming within dependently typed programming
• On the bright side of type classes: instance arguments in Agda
• Dependent Types at Work
• Cayenne -- a language with dependent types
• Implementing type theory in higher order constraint logic programming
• Cayenne -- a language with dependent types
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• Finiteness and rational sequences, constructively
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• PML2: integrated program verification in ML
• A correct-by-construction conversion from lambda calculus to combinatory logic
• scientific article; zbMATH DE number 7779291 (Why is no real title available?)
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Naïve Type Theory
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Admissible ordering on monomials is well-founded: a constructive proof
• Coalgebras in functional programming and type theory
• Specification and verification of a linear-time temporal logic for graph transformation
• Topological quantum gates in homotopy type theory
• Kripke-Joyal forcing for type theory and uniform fibrations
• Genetic programming + proof search = automatic improvement
• A syntax for mutual inductive families
• Deep induction for inductive families
• The size-change principle for mixed inductive and coinductive types
• Totality for mixed inductive and coinductive types
• The patch topology in univalent foundations
• Proof-relevant -calculus
• Proof-theoretic methods in quantifier-free definability
• Dependently typed array programs don't go wrong

This page was built for publication: Dependently typed programming in Agda

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3649136)