research
∙
09/21/2023
Stratified Type Theory
To exploit the expressivity of being able to refer to the type of types,...
share
research
∙
07/11/2022
Program Adverbs and Tlön Embeddings
Free monads (and their variants) have become a popular general-purpose t...
research
∙
07/05/2022
Implementing Dependent Types in pi-forall
These lecture notes describe the design of a minimal dependently-typed l...
research
∙
01/26/2022
A Dependent Dependency Calculus (Extended Version)
Over twenty years ago, Abadi et al. established the Dependency Core Calc...
research
∙
03/15/2021
ICFP 2020 Post-Conference Report
This document describes the ICFP 2020 virtual conference, including the ...
research
∙
03/12/2021
Reasoning about the garden of forking paths
Lazy evaluation is a powerful tool for functional programmers. It enable...
research
∙
10/25/2019
Embracing a mechanized formalization gap
If a code base is so big and complicated that complete mechanical verifi...
research
∙
05/31/2019
A Role for Dependent Types in Haskell (Extended version)
Modern Haskell supports zero-cost coercions, a mechanism where types tha...
research
∙
11/25/2017