The following pages link to (Q3477935):
Displaying 27 items.
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- Genetic programming \(+\) proof search \(=\) automatic improvement (Q682376) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation) (Q923069) (← links)
- Program development in constructive type theory (Q1190474) (← links)
- Recursive programming with proofs (Q1190480) (← links)
- Synthesis of ML programs in the system Coq (Q1322847) (← links)
- Classical logic, storage operators and second-order lambda-calculus (Q1326769) (← links)
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus (Q1329740) (← links)
- Automatizing termination proofs of recursively defined functions (Q1346629) (← links)
- The Inf function in the system \(F\) (Q1346636) (← links)
- A semantical storage operator theorem for all types (Q1382182) (← links)
- Additives of linear logic and normalization. I: A (restricted) Church-Rosser property. (Q1398477) (← links)
- System ST toward a type system for extraction and proofs of programs (Q1400600) (← links)
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models (Q1583485) (← links)
- About classical logic and imperative programming (Q1817076) (← links)
- The Girard-Reynolds isomorphism (Q1887154) (← links)
- Controlling Program Extraction in Light Logics (Q3007661) (← links)
- Lambda-calcul, évaluation paresseuse et mise en mémoire (Q3204440) (← links)
- First order marked types (Q4647574) (← links)
- Proof normalization modulo (Q4650285) (← links)
- On automating the extraction of programs from proofs using product types (Q4916212) (← links)
- Singleton, union and intersection types for program extraction (Q5096245) (← links)
- An ordinal measure based procedure for termination of functions (Q5940917) (← links)
- Completeness, minimal logic and programs extraction (Q5940922) (← links)
- Machine Deduction (Q6083700) (← links)
- Theoretical computer science: computability, decidability and logic (Q6602262) (← links)