The following pages link to Yannick Forster (Q1687734):
Displaying 13 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)
- Synthetic Kolmogorov complexity in coq (Q6572546) (← links)
- Constructive and synthetic reducibility degrees: Post's problem for many-one and truth-table reducibility in Coq (Q6610624) (← links)
