Typing termination in a higher-order concurrent imperative language

DOI10.1016/j.ic.2009.06.007zbMath1213.68159OpenAlexW2127169000MaRDI QIDQ979082

Gérard Boudol

Publication date: 25 June 2010

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2009.06.007

zbMATH Keywords

fairness property

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items

A Kripke logical relation for effect-based program transformations ⋮ Linear logical relations and observational equivalences for session-based concurrency ⋮ An Elementary Affine λ-Calculus with Multithreading and Side Effects

Uses Software

• ML
• Automath
• Esterel

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strong normalisation in the \(\pi\)-calculus
• Region-based memory management
• The Esterel synchronous programming language: Design, semantics, implementation
• The type and effect discipline
• A syntactic approach to type soundness
• Relational interpretations of recursive types in an operational setting.
• Syntactic Logical Relations for Polymorphic and Recursive Types
• Verification of non-functional programs using interpretations in type theory
• Relational Reasoning for Recursive Types and References
• Higher-Order Termination: From Kruskal to Computability
• Theoretical Aspects of Computing – ICTAC 2005
• Typing Safe Deallocation
• Termination of processes
• Frontiers of Combining Systems
• Programming Languages and Systems
• Intensional interpretations of functionals of finite type I
• Typed Lambda Calculi and Applications
• The Mechanical Evaluation of Expressions
• On the interpretation of intuitionistic number theory
• Programming Languages and Systems