Linked e-resources
Details
Table of Contents
Language Design
Consistent Subtyping for All
HOBiT: Programming Lenses without using Lens Combinators
Dualizing Generalized Algebraic Data Types by Matrix Transposition
Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach
Probabilistic Programming
An Assertion-Based Program Logic for Probabilistic Programs
Fine-grained Semantics for Probabilistic Programs
How long, O Bayesian network, will I sample thee?
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Types and Effects
Failure is Not an Option: An Exceptional Type Theory
Let Arguments Go First
Behavioural equivalence via modalities for algebraic effects
Explicit Effect Subtyping
Concurrency
A separation logic for a promising semantics
Logical Reasoning for Disjoint Permissions
Deadlock-Free Monitors
Fragment Abstraction for Concurrent Shape Analysis
Security
Reasoning About a Machine with Local Capabilities
Provably Safe Stack and Return Pointer Management
Modular Product Programs
Program Verification
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
Verified Learning Without Regret
Program Verification by Coinduction
Velisarios: Byzantine Fault Tolerant Protocols Powered by Coq
Program Analysis and Automated Verification
Evaluating Design Tradeoffs in Numeric Static Analysis for Java
An Abstract Interpretation Framework for Input Data Usage
Higher-Order Program Verification via HFL Model Checking
Quantitative Analysis of Smart Contracts
Session Types and Concurrency
Session-Typed Concurrent Contracts
A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
Concurrent Kleene Algebra: Free Model and Completeness
Concurrency and Distribution
Correctness of a Concurrent Object Collector for Actor Languages
Paxos Consensus, Deconstructed and Abstracted
On Parallel Snapshot Isolation and Release/Acquire Consistency
Eventual Consistency for CRDTs
Compiler Verification
A Verified Compiler from Isabelle/HOL to CakeML
Compositional Verification of Compiler Optimisations on Relaxed Memory.
Consistent Subtyping for All
HOBiT: Programming Lenses without using Lens Combinators
Dualizing Generalized Algebraic Data Types by Matrix Transposition
Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach
Probabilistic Programming
An Assertion-Based Program Logic for Probabilistic Programs
Fine-grained Semantics for Probabilistic Programs
How long, O Bayesian network, will I sample thee?
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Types and Effects
Failure is Not an Option: An Exceptional Type Theory
Let Arguments Go First
Behavioural equivalence via modalities for algebraic effects
Explicit Effect Subtyping
Concurrency
A separation logic for a promising semantics
Logical Reasoning for Disjoint Permissions
Deadlock-Free Monitors
Fragment Abstraction for Concurrent Shape Analysis
Security
Reasoning About a Machine with Local Capabilities
Provably Safe Stack and Return Pointer Management
Modular Product Programs
Program Verification
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
Verified Learning Without Regret
Program Verification by Coinduction
Velisarios: Byzantine Fault Tolerant Protocols Powered by Coq
Program Analysis and Automated Verification
Evaluating Design Tradeoffs in Numeric Static Analysis for Java
An Abstract Interpretation Framework for Input Data Usage
Higher-Order Program Verification via HFL Model Checking
Quantitative Analysis of Smart Contracts
Session Types and Concurrency
Session-Typed Concurrent Contracts
A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
Concurrent Kleene Algebra: Free Model and Completeness
Concurrency and Distribution
Correctness of a Concurrent Object Collector for Actor Languages
Paxos Consensus, Deconstructed and Abstracted
On Parallel Snapshot Isolation and Release/Acquire Consistency
Eventual Consistency for CRDTs
Compiler Verification
A Verified Compiler from Isabelle/HOL to CakeML
Compositional Verification of Compiler Optimisations on Relaxed Memory.