scientific article; zbMATH DE number 4147469
From MaRDI portal
Publication:3477935
zbMATH Open0699.68020MaRDI QIDQ3477935FDOQ3477935
Authors: Jean-Louis Krivine, Michel Parigot 
Publication date: 1990
Title of this publication is not available (Why is that?)
Recommendations
specificationsautomatic programmingcorrect programsmathematics as a programming languagesecond order intuitionistic
General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Second- and higher-order arithmetic and fragments (03F35)
Cited In (48)
- A semantical storage operator theorem for all types
- About classical logic and imperative programming
- Programming in Ωmega
- Different approaches to solving the problem of program correctness
- Genetic programming \(+\) proof search \(=\) automatic improvement
- Title not available (Why is that?)
- Singleton, union and intersection types for program extraction
- Lambda-calcul, évaluation paresseuse et mise en mémoire
- System ST toward a type system for extraction and proofs of programs
- PML2: integrated program verification in ML
- Proofs-as-programs as a framework for the design of an analogy-based ML editor
- 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
- Theoretical computer science: computability, decidability and logic
- Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
- The Girard-Reynolds isomorphism (second edition)
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- Logical and algorithmic formalisms for the problem of correct program design
- Tutorial on Subtype Marks
- Classical logic, storage operators and second-order lambda-calculus
- Programming language elements for correctness proofs
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- Title not available (Why is that?)
- Proofs verifying programs and programs producing proofs: a conceptual analysis
- Machine Deduction
- The Girard-Reynolds isomorphism
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus
- Title not available (Why is that?)
- 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
- Programming language elements for proof construction
- Comparing integrated and external logics of functional programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Synthesis of ML programs in the system Coq
- Title not available (Why is that?)
- Title not available (Why is that?)
- Code-carrying theories
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
- An ordinal measure based procedure for termination of functions
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)
