Automata-theoretic semantics of idealized Algol with passive expressions

DOI10.1016/j.entcs.2013.09.020zbMath1334.68040OpenAlexW2058372055WikidataQ113317952 ScholiaQ113317952MaRDI QIDQ265826

Uday S. Reddy

Publication date: 12 April 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2013.09.020

zbMATH Keywords

algebraic automata theoryfunctor categoriesidealized Algolreflexive graphsrelational parametricity

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Uses Software

• Dafny

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantics for concurrent separation logic
• Semantical analysis of specification logic
• Sheaves in geometry and logic: a first introduction to topos theory
• Categorical logic and type theory
• Full abstraction for idealized Algol with passive expressions
• Nominal Sets
• Syntactic control of interference for separation logic
• Dafny: An Automatic Program Verifier for Functional Correctness
• An Automata-Theoretic Model of Idealized Algol
• A model for syntactic control of interference
• Parametricity and local variables
• The impact of higher-order state and control effects on local relational reasoning
• A kripke logical relation for effect-based program transformations
• State-dependent representation independence
• Reading, Writing and Relations
• From Algol to polymorphic linear lambda-calculus