Publication:4603450

DOI10.23638/LMCS-14(1:11)2018zbMath1398.68080arXiv1710.09469MaRDI QIDQ4603450

Piotr Polesiuk, Dariusz Biernacki

Publication date: 20 February 2018

Full work available at URL: https://arxiv.org/abs/1710.09469

zbMATH Keywords

type system; logical relation; continuation-passing style; control effect; coherence of subtyping

Mathematics Subject Classification ID

68N15: Theory of programming languages

68N18: Functional programming and lambda calculus

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

Related Items

COCHIS: Stable and coherent implicits, Verifying Selective CPS Transformation for Shift and Reset

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inheritance as implicit coercion
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Classical logic, storage operators and second-order lambda-calculus
• Compositional semantics for composable continuations
• Delimited control and computational effects
• Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
• Axiomatizing Subtyped Delimited Continuations.
• The impact of higher-order state and control effects on local relational reasoning
• A very modal model of a modern, major, general type system
• Polymorphic Delimited Continuations
• Coherence of subsumption for monadic types
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Representing Control: a Study of the CPS Transformation
• Formulae-as-types for an involutive negation
• The coherence of languages with intersection types
• Subtyping delimited continuations
• State-dependent representation independence
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• Interactive proofs in higher-order concurrent separation logic
• Programming Languages and Systems