On the Relative Expressiveness of Higher-Order Session Processes
Abstract elided by the publisher.
976 papers · page 16 of 49
A Classical Realizability Model for a Semantical Value Restriction
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program propertie…
Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
Abstract elided by the publisher.
Simulating Cities: A Software Engineering Perspective
Abstract elided by the publisher.
Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
Abstract elided by the publisher.
Extensible and Efficient Automation Through Reflective Tactics
Abstract elided by the publisher.
An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs
Abstract elided by the publisher.
Functional Big-Step Semantics
Abstract elided by the publisher.
Classical By-Need
Abstract elided by the publisher.
Modular Termination Verification for Non-blocking Concurrency
Abstract elided by the publisher.
The Expressive Power of Monotonic Parallel Composition
Abstract elided by the publisher.
Macrofication: Refactoring by Reverse Macro Expansion
Abstract elided by the publisher.
Type Error Diagnosis for Embedded DSLs by Two-Stage Specialized Type Rules
Abstract elided by the publisher.
Actor Services - Modular Verification of Message Passing Programs
Abstract elided by the publisher.
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
Abstract elided by the publisher.
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specific…
Automatic Static Cost Analysis for Parallel Programs
Abstract elided by the publisher.
The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO
Abstract elided by the publisher.
Spatial Interpolants
We propose Splinter, a new technique for proving properties of heap-manipulating programs that marries (1) a new separation logic-based analysis for heap reasoning with (2) an interpolation-based technique for refining heap-shape invariants with data invariants. Splinter is prope…
The Problem of Programming Language Concurrency Semantics
Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while th…