The following pages link to (Q4435458):
Displaying 12 items.
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- Program extraction from normalization proofs (Q817701) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Intuitionistic fixed point logic (Q2220485) (← links)
- Flyspeck II: The basic linear programs (Q2379683) (← links)
- Controlling Program Extraction in Light Logics (Q3007661) (← links)
- Extraction of a program from deduction and its regularity. I (Q3726113) (← links)
- A realizability interpretation of Church's simple theory of types (Q4593235) (← links)
- Program extraction applied to monadic parsing (Q5225853) (← links)
- Studies of a theory of specifications with built-in program extraction (Q5951523) (← links)