Agda
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Advanced functional programming. 6th international school, AFP 2008, Heijen, The Netherlands, May 2008. Revised lectures
- Coq
- Cubical Agda
- Statebox
- CQL
- idris-ct
- Theorema
- Beluga
- CLEAN
- Isabelle/Isar
- Haskell
- Hammer for Coq: automation for dependent type theory
- MetaPRL
- Homotopy type theory in Lean
- From types to sets by local type definition in higher-order logic
- A consistent foundation for Isabelle/HOL
- Incorporating quotation and evaluation into Church's type theory
- The coinductive formulation of common knowledge
- HOL Light QE
- A formal equational theory for call-by-push-value
- An Agda formalization of Üresin \& Dubois' asynchronous fixed-point theory
- Undecidability of equality for codata types
- Biform theories: project description
- Matita
- CIRC
- Ivor
- HOL Light
- HOL-Omega
- A new implementation of Automath
- Nuprl
- Twelf
- Automath
- Lurch
- Trends in trends in functional programming 1999/2000 versus 2007/2008
- More dependent types for distributed arrays
- Type-specialized staged programming with process separation
- Machine learning guidance for connection tableaux
- ALF
- AutPGrp
- TRX
- Integrating induction and coinduction via closure operators and proof cycles
- Lilac
- FreshML
- From the universality of mathematical truth to the interoperability of proof systems
- Polyp
- \( \pi\) with leftovers: a mechanisation in Agda
- MetaOCaml
- Generic recursive lens combinators and their calculation laws
- Formalizing geometric algebra in Lean
- A certified program for the Karatsuba method to multiply polynomials
- The effects of effects on constructivism
- Coq/SSReflect
- Functions-as-constructors higher-order unification: extended pattern unification
- Camlflow
- Alfalfa
- iTasks
- Abella
- Cayenne
- Epigram
- Mella
- Irdis
- Flask
- CalcCheck
- Minlog
- System F in Agda, for fun and profit
- Herbrand constructivization for automated intuitionistic theorem proving
- AoPA
- A flexible categorial formalisation of term graphs as directed hypergraphs
- Coquet
- PhoX
- Milawa
- Galculator
- Constructing infinitary quotient-inductive types
- PoplMark
- Gmeta
- 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
- On a machine-checked proof for fraction arithmetic over a GCD domain
- Leveraging the information contained in theory presentations
- Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types
- Category theoretic structure of setoids
- Paco
- Towards specifying symbolic computation
- Automorphisms of types and their applications
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- Mechanized metatheory revisited
- Formalizing constructive projective geometry in Agda
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
- Formalization of universal algebra in Agda
- Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches
- AURA
- Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 -- July 1, 2015. Proceedings
- Formal metatheory of the lambda calculus using Stoughton's substitution
- A web-based toolkit for mathematical word processing applications with semantics
- Formalizing mathematical knowledge as a biform theory graph: a case study
- Automatically proving equivalence by type-safe reflection
- Formal derivation of greedy algorithms from relational specifications: a tutorial
- Nominal Isabelle
- An implementation of effective homotopy of fibrations
- Ynot
This page was built for software: Agda
