Agda

swMATH9689MaRDI QIDQ21668FDOQ21668

Author name not available (Why is that?)

Source code repository: https://github.com/agda/agda

Described by source

• Dependently typed programming in Agda

Cited In (only showing first 100 items - show all)

• Title not available (Why is that?)
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• From types to sets by local type definition in higher-order logic
• From the universality of mathematical truth to the interoperability of proof systems
• Leveraging the information contained in theory presentations
• From types to sets by local type definitions in higher-order logic
• Finiteness and rational sequences, constructively
• Automatically generating the dynamic semantics of gradually typed languages
• \( \pi\) with leftovers: a mechanisation in Agda
• Using Structural Recursion for Corecursion
• Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types
• 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
• Generic recursive lens combinators and their calculation laws
• A universe of binding and computation
• The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
• Normalisation by evaluation for type theory, in type theory
• Formalizing geometric algebra in Lean
• Incorporating quotation and evaluation into Church's type theory
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Trends in trends in functional programming 1999/2000 versus 2007/2008
• A Modular Type Reconstruction Algorithm
• A type theory for productive coprogramming via guarded recursion
• Eilenberg-MacLane spaces in homotopy type theory
• A certified program for the Karatsuba method to multiply polynomials
• The effects of effects on constructivism
• Extracting verified decision procedures: DPLL and resolution
• On irrelevance and algorithmic equality in predicative type theory
• Machine learning guidance for connection tableaux
• Indexed induction-recursion
• Productive coprogramming with guarded recursion
• A unification algorithm for Coq featuring universe polymorphism and overloading
• Type-specialized staged programming with process separation
• A formal equational theory for call-by-push-value
• The coinductive formulation of common knowledge
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• \(\Pi \Sigma \): dependent types without the sugar
• Irrelevance in type theory with a heterogeneous equality judgement
• Title not available (Why is that?)
• A henkin-style completeness proof for the modal logic S5
• Integrating induction and coinduction via closure operators and proof cycles
• Biform theories: project description
• Undecidability of equality for codata types
• Validating Brouwer's continuity principle for numbers using named exceptions
• Copatterns, programming infinite structures by observations
• Interactive programming in Agda -- objects and graphical user interfaces
• Bar induction is compatible with constructive type theory
• Indexed containers
• A verified theorem prover backend supported by a monotonic library
• Initial algebra semantics for cyclic sharing tree structures
• Formalizing constructive projective geometry in Agda
• System F in Agda, for fun and profit
• A light-weight integration of automated and interactive theorem proving
• Homotopy type theory in Lean
• Implementing type theory in higher order constraint logic programming
• A flexible categorial formalisation of term graphs as directed hypergraphs
• Well-founded recursion with copatterns and sized types
• Quotienting the delay monad by weak bisimilarity
• A formalized proof of strong normalization for guarded recursive types
• QED reloaded: towards a pluralistic formal library of mathematical knowledge
• A relaxation of Üresin and Dubois' asynchronous fixed-point theory in Agda
• Extensible and efficient automation through reflective tactics
• Algebra of programming in Agda: Dependent types for relational program derivation
• Combining proofs and programs in a dependently typed language
• Functions-as-constructors Higher-order Unification
• Higher homotopies in a hierarchy of univalent universes
• Cellular Cohomology in Homotopy Type Theory
• Constructing infinitary quotient-inductive types
• Intuitionistic completeness of first-order logic
• A logical framework combining model and proof theory
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Herbrand constructivization for automated intuitionistic theorem proving
• Genetic programming \(+\) proof search \(=\) automatic improvement
• Dependent Types at Work
• Dependent types and program equivalence
• Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
• A web-based toolkit for mathematical word processing applications with semantics
• Functional modelling of musical harmony: an experience report
• On a machine-checked proof for fraction arithmetic over a GCD domain
• Title not available (Why is that?)
• J-Calc: a typed lambda calculus for intuitionistic justification logic
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Mechanized metatheory revisited
• Functions-as-constructors higher-order unification: extended pattern unification
• Contributions to a computational theory of policy advice and avoidability
• Generative type abstraction and type-level computation
• Ivor, a Proof Engine
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Proof assistants for natural language semantics
• Synthesis of recursive ADT transformations from reusable templates
• Safe functional reactive programming through dependent types
• Category theoretic structure of setoids
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• 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
• A Focused Sequent Calculus for Higher-Order Logic
• Formal derivation of greedy algorithms from relational specifications: a tutorial
• Title not available (Why is that?)

This page was built for software: Agda