Typing termination in a higher-order concurrent imperative language

DOI10.1016/J.IC.2009.06.007MaRDI QIDQ979082zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Termination in higher-order concurrent calculi
• Termination in higher-order concurrent calculi
• Fair Cooperative Multithreading
• Ensuring termination by typability
• scientific article; zbMATH DE number 2163050

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 3513750 (Why is no real title available?)
• scientific article; zbMATH DE number 1948165 (Why is no real title available?)
• A syntactic approach to type soundness
• Frontiers of Combining Systems
• Higher-Order Termination: From Kruskal to Computability
• Intensional interpretations of functionals of finite type I
• On the interpretation of intuitionistic number theory
• Operational reasoning for functions with local state
• Programming Languages and Systems
• Programming Languages and Systems
• Region-based memory management
• Relational Reasoning for Recursive Types and References
• Relational interpretations of recursive types in an operational setting.
• Strong normalisation in the \(\pi\)-calculus
• Syntactic logical relations for polymorphic and recursive types
• Termination of processes
• The Esterel synchronous programming language: Design, semantics, implementation
• The Mechanical Evaluation of Expressions
• The type and effect discipline
• Theoretical Aspects of Computing – ICTAC 2005
• Typed Lambda Calculi and Applications
• Typing Safe Deallocation
• Verification of non-functional programs using interpretations in type theory

Cited in

(8)

• Fair Cooperative Multithreading
• Termination in higher-order concurrent calculi
• Termination in higher-order concurrent calculi
• Termination in impure concurrent languages
• Safe session-based concurrency with shared linear state
• A Kripke logical relation for effect-based program transformations
• Linear logical relations and observational equivalences for session-based concurrency
• An elementary affine \(\lambda \)-calculus with multithreading and side effects

Describes a project that uses

Uses Software

• ML
• Automath
• Esterel

This page was built for publication: Typing termination in a higher-order concurrent imperative language

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