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