A first order logic of effects

DOI10.1016/S0304-3975(97)00047-9MaRDI QIDQ1390955zbMATH OpenOpenAlexWikidataFDO

Authors 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

formal methodstheorem proving\(\lambda\)-calculusoperational semanticscontextsprogramming logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 515740
• A variable typed logic of effects
• A functional logic for higher level reasoning about computation
• scientific article; zbMATH DE number 86272

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 4148057 (Why is no real title available?)
• scientific article; zbMATH DE number 3827166 (Why is no real title available?)
• scientific article; zbMATH DE number 3909708 (Why is no real title available?)
• scientific article; zbMATH DE number 3687373 (Why is no real title available?)
• scientific article; zbMATH DE number 43015 (Why is no real title available?)
• scientific article; zbMATH DE number 89006 (Why is no real title available?)
• scientific article; zbMATH DE number 92599 (Why is no real title available?)
• scientific article; zbMATH DE number 3556031 (Why is no real title available?)
• scientific article; zbMATH DE number 515740 (Why is no real title available?)
• scientific article; zbMATH DE number 1032009 (Why is no real title available?)
• scientific article; zbMATH DE number 3995669 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 4189708 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A foundation for actor computation
• A theory for program and data type specification
• A theory of binding structures and applications to rewriting
• A variable typed logic of effects
• An application of open maps to categorical logic
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Can LCF be topped! Flat lattice models of typed \(\lambda{}\)-calculus
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Domain theory in logical form
• Equivalence in functional languages with effects
• Fast Decision Procedures Based on Congruence Closure
• From operational to denotational semantics
• Full abstraction and the Context Lemma (preliminary report)
• Full abstraction in the lazy lambda calculus
• Fully abstract models of typed \(\lambda\)-calculi
• Inferring the equivalence of functional programs that mutate data
• Isabelle. A generic theorem prover
• Logic, language and computation. Festschrift in Honor of Satoru Takasu
• Model theory
• Notions of computation and monads
• Prolegomena to a theory of mechanized formal reasoning
• REASONING ABOUT OBJECT SYSTEMS IN VTLoE
• Reasoning about functions with effects
• Ten Years of Hoare's Logic: A Survey—Part I
• The Mechanical Evaluation of Expressions
• The lambda calculus, its syntax and semantics
• The revised report on the syntactic theories of sequential control and state
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(5)

• A formalization of programs in first-order logic with a discrete linear order
• A variable typed logic of effects
• An observationally complete program logic for imperative higher-order functions
• Axioms for strict and lazy functional programs
• scientific article; zbMATH DE number 515740 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: A first order logic of effects

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