Programming Languages and Systems

- Typed Functional Programming

- Well-Typed Programs Can't Be Blamed

- Exploring the Design Space of Higher-Order Casts

- Practical Variable-Arity Polymorphism

- Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming

- ETAPS Invited Talk

- Using Category Theory to Design Programming Languages

- Computational Effects

- Modular Monad Transformers

- Handlers of Algebraic Effects

- Types for Object-Oriented Languages

- Is Structural Subtyping Useful? An Empirical Study

- An Interval-Based Inference of Variant Parametric Types

- Existential Quantification for Variant Ownership

- Verification

- Formalising and Verifying Reference Attribute Grammars in Coq

- Verified, Executable Parsing

- An Efficient Algorithm for Solving the Dyck-CFL Reachability Problem on Trees

- Amortised Memory Analysis Using the Depth of Data Structures

- ESOP Invited Talk

- The Financial Crisis, a Lack of Contract Specification Tools: What Can Finance Learn from Programming Language Design?

- Security

- All Secrets Great and Small

- Type-Based Automated Verification of Authenticity in Cryptographic Protocols

- Concurrency

- A Theory of Non-monotone Memory (Or: Contexts for free)

- Abstraction for Concurrent Objects

- Minimization Algorithm for Symbolic Bisimilarity

- Service-Oriented Computing

- Conversation Types

- Abstract Processes in Orchestration Languages

- Global Principal Typing in Partially Commutative Asynchronous Sessions

- Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services

- Parallel and Concurrent Programming

- Automatic Parallelization with Separation Logic

- Deny-Guarantee Reasoning

- A Basis for Verifying Multi-threaded Programs

- SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs