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
• Extracting verified decision procedures: DPLL and Resolution
• A Formalized Proof of Strong Normalization for Guarded Recursive Types
• 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
• Extensible and Efficient Automation Through Reflective Tactics
• 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
• Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
• Generic recursive lens combinators and their calculation laws
• A universe of binding and computation
• Higher Homotopies in a Hierarchy of Univalent Universes
• The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
• Formalizing geometric algebra in Lean
• Incorporating quotation and evaluation into Church's type theory
• Bar Induction is Compatible with Constructive Type Theory
• Trends in trends in functional programming 1999/2000 versus 2007/2008
• From Types to Sets by Local Type Definitions in Higher-Order Logic
• A Modular Type Reconstruction Algorithm
• A type theory for productive coprogramming via guarded recursion
• Interactive programming in Agda – Objects and graphical user interfaces
• Eilenberg-MacLane spaces in homotopy type theory
• A certified program for the Karatsuba method to multiply polynomials
• The effects of effects on constructivism
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• On irrelevance and algorithmic equality in predicative type theory
• Machine learning guidance for connection tableaux
• Indexed induction-recursion
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• 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
• Indexed containers
• 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 relaxation of Üresin and Dubois' asynchronous fixed-point theory in Agda
• Title not available (Why is that?)
• Copatterns
• 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
• 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
• Categories of Coalgebras with Monadic Homomorphisms
• A web-based toolkit for mathematical word processing applications with semantics
• On a machine-checked proof for fraction arithmetic over a GCD domain
• Coherence for Skew-Monoidal Categories
• Certified Parsing of Regular Languages
• 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
• Friends with Benefits
• 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
• Bisimulations Generated from Corecursive Equations
• A Consistent Foundation for Isabelle/HOL
• The Lean Theorem Prover (System Description)
• Ivor, a Proof Engine
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• A Constructive Model of Uniform Continuity
• Safe functional reactive programming through dependent types
• Partiality and recursion in interactive theorem provers – an overview
• POPLMark reloaded: Mechanizing proofs by logical relations
• Category theoretic structure of setoids
• Dependently-typed formalisation of relation-algebraic abstractions

This page was built for software: Agda