Scientific Papers & Books

Category Theory

• Seven Sketches in Compositionality: An Invitation to Applied Category Theory
• Category Theory for Scientists (Old Version)
• Categories for the Working Mathematician
• Cofree Traversable Functors
• Category Theory Using String Diagrams
• Category Theory
• Basic Category Theory

Type Theory

• Homotopy Type Theory: Univalent Foundations of Mathematics
• Type Systems for Programming Languages
• A Theory of Type Polymorphism in Programming
• Generalizing Hindley-Milner Type Inference Algorithms
• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
• Propositions as Types
• Theorems for Free!
• Typability and type checking in System F are equivalent and undecidable’
• Advanced Topics in Types and Programming Languages
• Type Theory & Functional Programming
• Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
• A Practical Subtyping System For Erlang
• Wobbly Types: Type Inference For Generalised Algebraic Data Types
• Proofs and Types
• In Search of Types
• Introduction to Univalent Foundations of Mathematics with Agda
• Bidirectional Typing
• Program = Proof
• Formal Topology in Univalent Foundations

Programming Language Theory (general)

• The Design and Implementation of Typed Scheme
• A Practical Type Checker for Scheme
• System F in Agda, for fun and profit
• From System F to Typed Assembly Language
• Type checking in the presence of meta-variables

Monads (general)

• Computational lambda-calculus and monads
• Monads for functional programming
• The essence of functional programming
• Imperative functional programming
• A Monad for Deterministic Parallelism
• Burritos for the Hungry Mathematician
• Toposes of Topological Monoid Actions

Comonads

• Comonadic Notions of Computation
• A Real-World Application with a Comonadic User Interface

Free Monads

• Freer Monads, More Extensible Effects
• Totality versus Turing-Completeness?

Type Checking

• Type checking and normalisation
• Type checking through unification
• Practical dependent type checking using twin types
• A Dependently-Typed Linear π-Calculus in Agda
• Co-Contextual Typing Inference for the Linear π-Calculus in Agda
• Mœbius: Metaprogramming using Contextual Types (link)
• Dependent pattern matching and proof-relevant unification (link)

Dependent Types

• Dependent Types in Haskell: Theory and Practice
• Certified Programming with Dependent Types
• A Tutorial Implementation of a Dependently Typed Lambda Calculus
• Higher-Order Dynamic Pattern Unification for Dependent Types and Records
• Dependently Typed Programming in Agda

Linear Types

• Composable Efficient Array Computations Using Linear Types
• On the Duality of Streams: How Can Linear Types Help to Solve the Lazy IO Problem?
• Linear types can change the world!
• Destination-passing style programming: a Haskell implementation (link)

Pi-calculus

• A DISTRIBUTED pi-calculus (link)
• Communicating Sequential Processes (link)

Fudgets

• Lazy Functional Components for Graphical User Interfaces

NixOS

• NixOS: A Purely Functional Linux Distribution (link)
• The Purely Functional Software Deployment Model (link)

Cubical Type Theory

• Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom
• Finiteness in Cubical Type Theory

API design

• Functional Pearls Ghosts of Departed Proofs

Transient State Electronics

• Recent development of transient electronics
• Transient Electronics as Sustainable Systems: From Fundamentals to Applications

Quantum Theory and Proofs

• An Effect-Theoretic Reconstruction of Quantum Theory
• MIP* = R
• International Symposium on Mathematics, Quantum Theory, and Cryptography (2019)
• Inference, interference and invariance: How the Quantum Fourier Transform can help to learn from data (link)

Non-terrestrial Quantum Networks

• A survey on non-terrestrial quantum networking: Challenges and trends (link)

Uncategorized

• The Implementation of Functional Programming Languages
• Haskell SpriteKit
• QED at Large: A Survey of Engineering of Formally Verified Software
• A Block Design for Introductory Functional Programming in Haskell
• Efficient Functional Programming using Linear Types: The Array Fragment
• Exploring Generic Haskell
• Verified Functional Programming in Agda
• Retrofitting Linear Types
• The History of Standard ML
• A Calculus of Mobile Processes, I & II
• Efficient Communication and Collection with Compact Normal Form
• Purely Functional Data Structures
• How to write a Finanial Contract
• Composing Contracts: An Adventure in Financial Engineering
• How to Keep Your Neighbours in Order
• On the Bright Side of Type Classes: Instance Arguments in Agda
• The Undecidability of BB(748) (link)
• HASKELL The Craft of Functional Programming (link)
• Understanding and Evolving the ML Module System (link)
• Mathematics for Computer Science (link)
• A Modern Compiler for the French Tax Code (link)
• The Knowledge Complexity of Interactive Proof Systems (link)
• The Calculus of Constructions (link)
• Smart Reduction (link)