Pages that link to "Item:Q3649136"

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

Displayed 31 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)
• Incorporating quotation and evaluation into Church's type theory (Q1753993) ‎ (← 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 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)
• 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)
• 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)