The following pages link to Yannick Forster (Q1687734):
Displayed 14 items.
- Weak call-by-value lambda calculus as a model of computation in Coq (Q1687735) (← links)
- Verification of PCP-related computational reductions in Coq (Q1791165) (← links)
- Parametric Church's thesis: synthetic computability without choice (Q2151397) (← links)
- Completeness theorems for first-order logic analysed in constructive type theory (Q2177578) (← links)
- The \textsc{MetaCoq} project (Q2209542) (← links)
- Call-by-value lambda calculus as a model of computation in Coq (Q2319993) (← links)
- Completeness theorems for first-order logic analysed in constructive type theory (Q5028312) (← links)
- Hilbert's Tenth Problem in Coq (Q5089029) (← links)
- (Q5094119) (← links)
- A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus (Q5875425) (← links)
- (Q6099607) (← links)
- Formal small-step verification of a call-by-value lambda calculus machine (Q6166150) (← links)
- Parametric Church's Thesis: Synthetic Computability without Choice (Q6386412) (← links)
- Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions (Q6445465) (← links)