Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

DOI10.1016/J.JLAP.2012.01.004zbMATH Open1259.03044arXiv1112.2950OpenAlexW1967996089MaRDI QIDQ444460FDOQ444460

Authors: E. Polonowski, T. Crolard 

Publication date: 14 August 2012

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Abstract: We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order procedural variables from a formul{ae}-as-types notion of control for classical logic. The main contribution of this work is the design of an imperative dependent type system for non-local jumps which corresponds to classical logic but where the famous consequence rule is still derivable.

Full work available at URL: https://arxiv.org/abs/1112.2950

Recommendations

• Program logics for sequential higher-order control
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2154396
• Programming Languages and Systems
• scientific article; zbMATH DE number 1500648

zbMATH Keywords

continuationmonadFloyd-Hoare logiccallcchigher-order procedureimperative dependent type system for Hoare triplesnon-local jumps

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Ynot: dependent types for imperative programs
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A judgmental reconstruction of modal logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• From Algol to polymorphic linear lambda-calculus
• Title not available (Why is that?)
• Notions of computation and monads
• Lectures on the Curry-Howard isomorphism
• An axiomatic basis for computer programming
• Ten Years of Hoare's Logic: A Survey—Part I
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verification, Model Checking, and Abstract Interpretation
• Refined program extraction from classical proofs
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• A sound and relatively* complete Hoare-logic for a language with higher type procedures
• Program logics for sequential higher-order control
• Descriptive and Relative Completeness of Logics for Higher-Order Functions
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Correspondence between ALGOL 60 and Church's Lambda-notation
• The Mechanical Evaluation of Expressions
• Automata, Languages and Programming
• Proofs of strong normalisation for second order classical natural deduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Continuations in possible-world semantics
• 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
• Practical program extraction from classical proofs
• Extending the loop language with higher-order procedural variables
• A Hoare Logic for the State Monad
• Title not available (Why is that?)
• A critique of the foundations of Hoare style programming logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computational types from a logical perspective
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Formulae-as-Types Interpretation of Subtractive Logic
• Title not available (Why is that?)
• Control effects as a modality
• Polymorphism and separation in Hoare type theory
• Typed Lambda Calculi and Applications
• Proofs-as-imperative-programs: application to synthesis of contracts
• Intrinsic reasoning about functional programs. I: First order theories

Cited In (2)

• Programming and Proving with Classical Types
• Program logics for sequential higher-order control

Uses Software

• SPARK
• Nuprl
• Twelf
• Z
• Ynot
• ALGOL 60

This page was built for publication: Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q444460)