The following pages link to Agda (Q21668):
Displaying 50 items.
- J-Calc: a typed lambda calculus for intuitionistic justification logic (Q276037) (← links)
- A constructive manifestation of the Kleene-Kreisel continuous functionals (Q290639) (← links)
- Formalizing semantic bidirectionalization and extensions with dependent types (Q347391) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Certified CYK parsing of context-free languages (Q465493) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Constructions of categories of setoids from proof-irrelevant families (Q512135) (← links)
- Flag-based big-step semantics (Q516041) (← links)
- Pointfree expression and calculation: From quantification to temporal logic (Q633283) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Genetic programming \(+\) proof search \(=\) automatic improvement (Q682376) (← links)
- Isomorphism is equality (Q740487) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Q834373) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Advanced functional programming. 6th international school, AFP 2008, Heijen, The Netherlands, May 2008. Revised lectures (Q1030977) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Homotopy type theory in Lean (Q1687770) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- The coinductive formulation of common knowledge (Q1791151) (← links)
- HOL Light QE (Q1791161) (← links)
- A formal equational theory for call-by-push-value (Q1791198) (← links)
- An Agda formalization of Üresin \& Dubois' asynchronous fixed-point theory (Q1791213) (← links)
- Undecidability of equality for codata types (Q1798783) (← links)
- Biform theories: project description (Q1798949) (← links)
- A new implementation of Automath (Q1868514) (← links)
- Trends in trends in functional programming 1999/2000 versus 2007/2008 (Q1929344) (← links)
- More dependent types for distributed arrays (Q1929345) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- \( \pi\) with leftovers: a mechanisation in Agda (Q2117018) (← links)
- Generic recursive lens combinators and their calculation laws (Q2123055) (← links)
- Formalizing geometric algebra in Lean (Q2128117) (← links)
- A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
- The effects of effects on constructivism (Q2133168) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- System F in Agda, for fun and profit (Q2176683) (← links)
- Herbrand constructivization for automated intuitionistic theorem proving (Q2180528) (← links)
- A flexible categorial formalisation of term graphs as directed hypergraphs (Q2185888) (← links)
- Constructing infinitary quotient-inductive types (Q2200826) (← links)
- A relaxation of Üresin and Dubois' asynchronous fixed-point theory in Agda (Q2209538) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- On a machine-checked proof for fraction arithmetic over a GCD domain (Q2217198) (← links)
- Leveraging the information contained in theory presentations (Q2219380) (← links)
- Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types (Q2229149) (← links)
- Category theoretic structure of setoids (Q2253183) (← links)
