A first order logic of effects

DOI10.1016/S0304-3975(97)00047-9zbMath0901.68182OpenAlexW2088336357MaRDI QIDQ1390955

Ian A. Mason

Publication date: 22 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(97)00047-9

zbMATH Keywords

operational semanticstheorem provingformal methods\(\lambda\)-calculuscontextsprogramming logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items

An observationally complete program logic for imperative higher-order functions ⋮ Axioms for strict and lazy functional programs

Uses Software

• Isabelle

Cites Work

• A theory of binding structures and applications to rewriting
• Using typed lambda calculus to implement formal systems on a machine
• Notions of computation and monads
• An application of open maps to categorical logic
• Prolegomena to a theory of mechanized formal reasoning
• The lambda calculus, its syntax and semantics
• Domain theory in logical form
• Inferring the equivalence of functional programs that mutate data
• The revised report on the syntactic theories of sequential control and state
• A theory for program and data type specification
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Fully abstract models of typed \(\lambda\)-calculi
• Full abstraction in the lazy lambda calculus
• Logic, language and computation. Festschrift in Honor of Satoru Takasu
• Isabelle. A generic theorem prover
• Model theory
• Can LCF be topped! Flat lattice models of typed \(\lambda{}\)-calculus
• A variable typed logic of effects
• Fast Decision Procedures Based on Congruence Closure
• Ten Years of Hoare's Logic: A Survey—Part I
• A foundation for actor computation
• REASONING ABOUT OBJECT SYSTEMS IN VTLoE
• Equivalence in functional languages with effects
• Full abstraction and the Context Lemma (preliminary report)
• Decidability of Second-Order Theories and Automata on Infinite Trees
• The Mechanical Evaluation of Expressions
• From operational to denotational semantics
• 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