Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
DOI10.1016/j.jlap.2012.01.004zbMath1259.03044arXiv1112.2950OpenAlexW1967996089MaRDI QIDQ444460
E. Polonowski, Tristan Crolard
Publication date: 14 August 2012
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1112.2950
continuationmonadFloyd-Hoare logiccallcchigher-order procedureimperative dependent type system for Hoare triplesnon-local jumps
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Uses Software
Cites Work
- Notions of computation and monads
- Lectures on the Curry-Howard isomorphism
- A sound and relatively* complete Hoare-logic for a language with higher type procedures
- Continuations in possible-world semantics
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Locations considered unnecessary
- System \(T\), call-by-value and the minimum problem
- Revised report on the algorithmic language scheme
- An introduction to Landin's ``A generalization of jumps and labels
- A generalization of jumps and labels
- Classical logic, storage operators and second-order lambda-calculus
- Deriving proof rules from continuation semantics
- Hoare logic and auxiliary variables
- Program proving: KJumps and functions
- A judgmental reconstruction of modal logic
- Extending the loop language with higher-order procedural variables
- A Hoare Logic for the State Monad
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Program Logics for Sequential Higher-Order Control
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Ten Years of Hoare's Logic: A Survey—Part I
- A critique of the foundations of Hoare style programming logics
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Computational types from a logical perspective
- Proofs of strong normalisation for second order classical natural deduction
- A Formulae-as-Types Interpretation of Subtractive Logic
- Ynot
- Control effects as a modality
- Correspondence between ALGOL 60 and Church's Lambda-notation
- From Algol to polymorphic linear lambda-calculus
- Polymorphism and separation in hoare type theory
- An axiomatic basis for computer programming
- Typed Lambda Calculi and Applications
- Automata, Languages and Programming
- The Mechanical Evaluation of Expressions
- Verification, Model Checking, and Abstract Interpretation
- Perspectives of System Informatics
- Refined program extraction from classical proofs
- Intrinsic reasoning about functional programs. I: First order theories
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
