Cited in
(only showing first 100 items - show all)- A mechanised abstract formalisation of concept lattices
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- Higher homotopies in a hierarchy of univalent universes
- Intuitionistic completeness of first-order logic
- Constructing infinitary quotient-inductive types
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- On the bright side of type classes: instance arguments in Agda
- Cellular Cohomology in Homotopy Type Theory
- scientific article; zbMATH DE number 2090016 (Why is no real title available?)
- Characteristics of de Bruijn’s early proof checker Automath
- A logical framework combining model and proof theory
- Herbrand constructivization for automated intuitionistic theorem proving
- A module calculus for Pure Type Systems
- Partiality and Container Monads
- Genetic programming + proof search = automatic improvement
- From types to sets by local type definition in higher-order logic
- Types for Proofs and Programs
- From the universality of mathematical truth to the interoperability of proof systems
- Leveraging the information contained in theory presentations
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
- Dependent Types at Work
- Dependent types and program equivalence
- From types to sets by local type definitions in higher-order logic
- A web-based toolkit for mathematical word processing applications with semantics
- On a machine-checked proof for fraction arithmetic over a GCD domain
- Functional modelling of musical harmony: an experience report
- J-Calc: a typed lambda calculus for intuitionistic justification logic
- scientific article; zbMATH DE number 7199581 (Why is no real title available?)
- Program calculation in Coq
- Formalization of universal algebra in Agda
- Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches
- Generic programming with dependent types
- scientific article; zbMATH DE number 1420784 (Why is no real title available?)
- Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
- Functions out of higher truncations
- Nameless, painless
- \( \pi\) with leftovers: a mechanisation in Agda
- Editorial: Special issue on programming with dependent types
- Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types
- Dependently Typed Programming Based on Automated Theorem Proving
- Finiteness and rational sequences, constructively
- Automatically generating the dynamic semantics of gradually typed languages
- Using Structural Recursion for Corecursion
- Heterogeneous binary random-access lists
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Mechanized metatheory revisited
- Types for Proofs and Programs
- Functions-as-constructors higher-order unification: extended pattern unification
- A mechanized textbook proof of a type unification algorithm
- Generic recursive lens combinators and their calculation laws
- Automating theorem proving with SMT
- On the Mints hierarchy in first-order intuitionistic logic
- Sorted. Verifying the problem of the Dutch national flag in Agda
- The lax braided structure of streaming I/O
- Contributions to a computational theory of policy advice and avoidability
- A universe of binding and computation
- Galois Connections for Recursive Types
- Generative type abstraction and type-level computation
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- Formalizing geometric algebra in Lean
- A constructive manifestation of the Kleene-Kreisel continuous functionals
- Incorporating quotation and evaluation into Church's type theory
- Ivor, a Proof Engine
- Normalisation by evaluation for type theory, in type theory
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Auto in Agda. Programming proof search using reflection
- Proof assistants for natural language semantics
- Synthesis of recursive ADT transformations from reusable templates
- Trends in trends in functional programming 1999/2000 versus 2007/2008
- Dependently Typed Grammars
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- Safe functional reactive programming through dependent types
- Exercising Nuprl's open-endedness
- A certified program for the Karatsuba method to multiply polynomials
- The effects of effects on constructivism
- Wellfounded recursion with copatterns: a unified approach to termination and productivity
- A Modular Type Reconstruction Algorithm
- A type theory for productive coprogramming via guarded recursion
- From realizability to induction via dependent intersection
- Eilenberg-MacLane spaces in homotopy type theory
- Sequential decision problems, dependent types and generic solutions
- Dot-types and their implementation
- A pattern for almost compositional functions
- Category theoretic structure of setoids
- On irrelevance and algorithmic equality in predicative type theory
- Extracting verified decision procedures: DPLL and resolution
- Machine learning guidance for connection tableaux
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- Indexed induction-recursion
- Dependently-typed formalisation of relation-algebraic abstractions
- Towards certifiable implementation of graph transformation via relation categories
- More dependent types for distributed arrays
- Isomorphism is equality
- Quotients, inductive types, and quotient inductive types
- Extracting a DPLL algorithm
- Automatically proving equivalence by type-safe reflection
- Implementing Cantor's paradise
This page was built for software: Agda
