Research Activities

PhD manuscript

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings

Thomas Bagrel

Destination-passing style programming introduces destinations that let callers control memory management while preserving a pure functional setting.

• type systems
• haskell

PaperArxiv

IFL 2025

Refinement-Types Driven Development: A study

Facundo Domínguez, Arnaud Spiwack

A study of how SMT-backed refinement types can extend ordinary type checking for program composition.

• types in practice
• haskell
• liquid haskell

PaperArxiv

OlivierFest'25

Invertible Syntax without the Tuples (Functional Pearl)

Mathieu Boespflug, Arnaud Spiwack

A continuation-passing approach to invertible syntax descriptions that parse and print structured data without dependent types or nested-pair aggregation.

• haskell

PaperArxiv

OOPSLA1 2025

Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes

Thomas Bagrel, Arnaud Spiwack

A pure functional calculus for destination passing, using linearity to reason about memory writes.

• type systems
• performance

PaperArxiv

JFLA 2024

Destination-passing style programming: a Haskell implementation

Thomas Bagrel

A Haskell implementation of destination-passing style programming for caller-controlled memory management.

• haskell
• type systems

Arxiv

FUNARCH 2023

Crème de la Crem: Composable Representable Executable Machines

Marco Perone, Georgios Karachalias

A compositional state-machine approach to software architecture, grounded in Domain-Driven Design.

• haskell

PaperArxiv

ITP 2023

No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System

Roger Bosman, Georgios Karachalias, Tom Schrijvers

A mechanically verified account of fully grounding type inference for the Hindley-Damas-Milner system.

• haskell
• type systems

Paper

ICFP 2022

Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control Flow

Norman Ramsey

A recursive single-pass translation from arbitrary compiler control flow to structured control flow.

• haskell
• wasm

Paper

ICFP 2022

Linearly Qualified Types: Generic inference for capabilities and uniqueness

Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg

A qualified type system and inference algorithm for reducing the overhead of programming with linear types.

• haskell
• type systems

PaperArxiv

Conditionally accepted at POPL 2022

Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation

Faustyna Krawiec, Neel Krishnaswami, Simon Peyton-Jones, Tom Ellis, Andrew Fitzgibbon, Richard A. Eisenberg

A simple implementation of reverse-mode automatic differentiation for higher-order functions with linear runtime and memory use.

• haskell
• machine learning

Dynamic Language Symposium 2021

Union and intersection contracts are hard, actually

Teodoro Freund, Yann Hamdaoui, Arnaud Spiwack

A survey and explanation of the tradeoffs behind higher-order contracts with union and intersection types.

• type systems
• nickel

Arxiv

OOPSLA 2021

Efficient Compilation of Algebraic Effect Handlers

Georgios Karachalias, Filip Koprivec, Matija Pretnar, Tom Schrijvers

Type-and-effect directed optimising compilation for narrowing the performance gap around algebraic effect handlers.

• ocaml
• effects

PaperZenodo

Haskell Symposium 2021

Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation is user friendly

Gert-Jan Bottu, Richard A. Eisenberg

An analysis of polymorphic instantiation approaches in GHC/Haskell through the lens of program stability.

• haskell
• type systems

Paper

Haskell Symposium 2021

Evaluating Linear Functions to Symmetric Monoidal Categories

Jean-Philippe Bernardy, Arnaud Spiwack

A library approach to embedded languages expressed as diagrams, using linear functions and symmetric monoidal categories.

• haskell
• types in practice

PaperArxiv

ICFP 2021 (Distinguished Paper)

An Existential Crisis Resolved: Type inference for first-class existential types

Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, Daniel Lee

A bidirectional type-inference algorithm for introducing and eliminating first-class existential types.

• haskell
• type systems

Paper

POPL 2020

Partial Type Constructors; Or, Making ad hoc datatypes less ad hoc

Mark P. Jones, J. Garrett Morris, Richard A. Eisenberg

A language design and formal theory for partial type constructors using qualified types.

• haskell
• type systems

Paper

POPL 2021

A Graded Dependent Type System with a Usage-Aware Semantics

Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, Stephanie Weirich

A graded dependent type system with operational semantics that account for resource usage.

• haskell
• type systems

PaperArxiv

OOPSLA 2020

Resolution as Intersection Subtyping via Modus Ponens

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, Georgios Karachalias

A calculus showing how subtyping with intersection types can subsume resolution mechanisms.

• type systems

PaperArxivZenodo

Haskell Symposium 2020

Composing Effects into Tasks and Workflows

Yves Parès, Jean-Philippe Bernardy, Richard A. Eisenberg

An effect-handler and arrow-inspired design for modular data-science workflows.

• haskell
• machine learning
• types in practice

Paper

Haskell Symposium 2020

Stitch: The Sound Type-Indexed Type Checker, a Functional Pearl

Richard A. Eisenberg

A modern Haskell interpreter and type checker that demonstrates practical use of advanced type-indexed techniques.

• haskell
• types in practice

Paper

ICFP 2020

Kinds are Calling Conventions

Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg

An intermediate language that encodes calling-convention information in kinds for efficient static compilation.

• haskell
• performance

Paper

POPL 2020 (Distinguished Paper)

Kind Inference for Datatypes

Ningning Xie, Richard A. Eisenberg, Bruno C. d. S. Oliveira

Declarative and algorithmic specifications for principled kind inference of datatype declarations.

• haskell
• type systems

Paper

POPL 2018

Linear Haskell: practical linearity in a higher-order polymorphic language

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack

A backwards-compatible linear type system integrated into Haskell via linear function arrows.

• haskell
• type systems

PaperArxiv

IFL 2014

Programming R in Haskell

Mathieu Boespflug, Allen Brown, Facundo Domínguez, Alexander Vershilov

An R-to-Haskell interoperability approach that makes R libraries available from statically typed Haskell programs.

• haskell
• language interop

PaperHomepage