A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus (Q5875425)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus |
scientific article; zbMATH DE number 7649966
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A certifying extraction with time bounds from Coq to call-by-value
$\lambda$-calculus |
scientific article; zbMATH DE number 7649966 |
Statements
3 February 2023
0 references
call-by-value
0 references
\(\lambda\) calculus
0 references
Coq
0 references
constructive type theory
0 references
extraction
0 references
computability
0 references
A certifying extraction with time bounds from Coq to call-by-value
$\lambda$-calculus (English)
0 references
