Programming Languages and Systems

Disjoint Polymorphism.- Generalizing inference systems by coaxioms.- Observed Communication Semantics for Classical Processes.- Is your software on dope? - Formal analysis of surreptitiously "enhanced" programs.- Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants.- Confluence of Graph Rewriting with Interfaces.- Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency.- Incremental update for graph rewriting.- Linearity, Control Effects, and Behavioral Types.- Temporary Read-Only Permissions for Separation Logic.- Faster Algorithms for Weighted Recursive State Machines.- ML and Extended BVASS. - Metric Reasoning about Lambda Terms: the General Case.- Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring.- Probabilistic Termination by Monadic Affine Sized Typing.- Caper: Automatic Verification for Fine-grained Concurrency.- Tackling Real-Life Relaxed Concurrency with FSL++. - Extensible DatasortRefinements.- Programs Using Syntax with First-Class Binders. - Lincx: A Linear Logical Framework with First-class Context.- APLicative Programming with Naperian Functors.- Verified Characteristic Formulae for CakeML.- Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic.- Proving Linearizability Using Partial Orders.- The Power of Non-Determinism in Higher-Order Implicit Complexity.- The Essence of Higher-Order Concurrent Separation Logic.- Comprehending Isabelle/HOL's Consistency.-The essence of functional programming on semantic data.- A Classical Sequent Calculus with Dependent Types.- Context-Free Session Type Inference.- Modular Verification of Higher-order Functional Programs.- Commutative semantics for probabilistic programming.- Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization.- A Higher-Order Logic for Concurrent Termination-Preserving Refinement.- Modular Verification of Procedure Equivalence in the