scientific article; zbMATH DE number 4147469
From MaRDI portal
Publication:3477935
Recommendations
Cited in
(48)- Proving properties of Pascal programs in MIZAR 2
- Program development in constructive type theory
- Recursive programming with proofs
- Synthesis of ML programs in the system Coq
- Classical logic, storage operators and second-order lambda-calculus
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus
- Automatizing termination proofs of recursively defined functions
- The Inf function in the system \(F\)
- A semantical storage operator theorem for all types
- Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
- System ST toward a type system for extraction and proofs of programs
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- About classical logic and imperative programming
- The Girard-Reynolds isomorphism
- Code-carrying theories
- Joining programming theorems. A practical approach to program building
- Controlling Program Extraction in Light Logics
- Programming language elements for proof construction
- Different approaches to solving the problem of program correctness
- scientific article; zbMATH DE number 4172362 (Why is no real title available?)
- Lambda-calcul, évaluation paresseuse et mise en mémoire
- Proofs as programs
- Programming in Ωmega
- Programming language elements for correctness proofs
- Proofs verifying programs and programs producing proofs: a conceptual analysis
- scientific article; zbMATH DE number 4006266 (Why is no real title available?)
- scientific article; zbMATH DE number 140006 (Why is no real title available?)
- scientific article; zbMATH DE number 517012 (Why is no real title available?)
- scientific article; zbMATH DE number 1973214 (Why is no real title available?)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- scientific article; zbMATH DE number 2079677 (Why is no real title available?)
- First order marked types
- Proof normalization modulo
- scientific article; zbMATH DE number 4113956 (Why is no real title available?)
- On automating the extraction of programs from proofs using product types
- Singleton, union and intersection types for program extraction
- Tutorial on Subtype Marks
- Logical and algorithmic formalisms for the problem of correct program design
- An ordinal measure based procedure for termination of functions
- Completeness, minimal logic and programs extraction
- PML2: integrated program verification in ML
- Machine Deduction
- Theoretical computer science: computability, decidability and logic
- Genetic programming + proof search = automatic improvement
- Proofs-as-programs as a framework for the design of an analogy-based ML editor
- The Girard-Reynolds isomorphism (second edition)
- Comparing integrated and external logics of functional programs
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3477935)
