Pages that link to "Item:Q3649136"
From MaRDI portal
The following pages link to Dependently Typed Programming in Agda (Q3649136):
Displayed 45 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)
- 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)
- (Q6068929) (← links)
- Naïve Type Theory (Q6075423) (← links)
- Admissible ordering on monomials is well-founded: a constructive proof (Q6094419) (← links)