Pages that link to "Item:Q3649136"

The following pages link to Dependently Typed Programming in Agda (Q3649136):

Displaying 49 items.

• Agda (Q21668) (← links)
• 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)
• Certified CYK parsing of context-free languages (Q465493) (← links)
• Coalgebras in functional programming and type theory (Q639643) (← links)
• Genetic programming \(+\) proof search \(=\) automatic improvement (Q682376) (← links)
• Dependently typed array programs don't go wrong (Q843222) (← links)
• Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
• A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
• On a machine-checked proof for fraction arithmetic over a GCD domain (Q2217198) (← links)
• Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types (Q2229149) (← links)
• Formalizing constructive projective geometry in Agda (Q2333313) (← links)
• A web-based toolkit for mathematical word processing applications with semantics (Q2364686) (← links)
• Formalizing mathematical knowledge as a biform theory graph: a case study (Q2364688) (← links)
• A henkin-style completeness proof for the modal logic S5 (Q2695534) (← links)
• A Classical Realizability Model for a Semantical Value Restriction (Q2802494) (← links)
• Type theory should eat itself (Q2804938) (← links)
• Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Q2817296) (← links)
• Auto in Agda (Q2941181) (← links)
• Program Calculation in Coq (Q3067474) (← links)
• Bisimulations Generated from Corecursive Equations (Q3178257) (← links)
• A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520) (← links)
• Galois Connections for Recursive Types (Q3297839) (← links)
• Synthesis of Recursive ADT Transformations from Reusable Templates (Q3303897) (← links)
• (Q3384910) (← links)
• The Lean Theorem Prover (System Description) (Q3454108) (← links)
• Quotienting the delay monad by weak bisimilarity (Q4559601) (← links)
• Proof-relevant π-calculus: a constructive account of concurrency and causality (Q4691184) (← links)
• COCHIS: Stable and coherent implicits (Q4972074) (← links)
• (Q5013829) (← links)
• Higher order functions and Brouwer’s thesis (Q5016215) (← links)
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
• A greedy algorithm for dropping digits (Q5020906) (← links)
• Partiality and Container Monads (Q5056003) (← links)
• POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
• Heterogeneous binary random-access lists (Q5110935) (← links)
• Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007) (← links)
• Finiteness and rational sequences, constructively (Q5372009) (← links)
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic (Q6060672) (← links)
• (Q6060675) (← links)
• A correct-by-construction conversion from lambda calculus to combinatory logic (Q6065511) (← links)
• (Q6068934) (← links)
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules (Q6079228) (← links)
• Admissible ordering on monomials is well-founded: a constructive proof (Q6094419) (← links)
• Specification and verification of a linear-time temporal logic for graph transformation (Q6535505) (← links)
• Topological quantum gates in homotopy type theory (Q6584358) (← links)
• Kripke-Joyal forcing for type theory and uniform fibrations (Q6586829) (← links)