Talks

A well-known representation of monoids and its application to the function “vector reverse”
ICFP. Remote presentation.
Purely functional, fully in-place programming
SWS Seminar. Nijmegen.
Purely functional, fully in-place programming
Algorithms Seminar. Utrecht.
How to believe a verified program?
Unsound Workshop. Remote.
A correct-by-construction conversion to combinators
IFIP WG 2.1. Online.
Calculating datastructures
Mathematics of Program Construction. Remote.
A predicate transformer semantics for effects
Delft Colloquium. Remote.
Generic enumerations: completely, fairly
IFIP WG 2.1. Online.
Heterogeneous binary random access lists
JFP track of ICFP 2020. Remote.
A predicate transformer semantics for effects
A research agenda for formal methods in the Netherlands. Lorentz Center, Leiden, the Netherlands.
A predicate transformer semantics for effects
ICFP 2019. Berlin, Germany.
From algebra to abstract machine
IFIP WG 2.1. Brandenburg, Germany.
Data types à la carte
Cross Functional Amsterdam Meetup. Amsterdam, the Netherlands.
Structured diffs: theory and practice
ICFP PC Meeting. Salt Lake City, UT.
Algebraic effects - specification and refinement
Dagstuhl meeting. Schloss Dagstuhl.
Calculating correct programs
Meeting of the EU TYPES Cost Action. Nijmegen, the Netherlands.
Embedding the refinement calculus in Coq
IFIP WG 2.1. Lesbos, Greece.
Type directed diffing of structured data
TyDe. Oxford, UK.
Datatype Generic Packet Descriptions
Galois Tech Talk. Portland, Oregon.
QuickCheck: a lightweight tool for random testing Haskell programs
Papers we love. Utrecht, the Netherlands.
PiWare: A hardware description language embedded in Agda
IFIP WG 2.1 Meeting. Glasgow, UK.
Lazy, staged binary decision diagrams
Dagstuhl Seminar 16131 on Language Based Verification Tools for Functional Programs. Schloss Dagstuhl, Germany.
From proposition to program
International Symposium on Functional and Logic Programming (FLOPS '16). Kochi, Japan.
Auto in Agda
Workshop on Advances in Programming Languages and Systems. Frankfurt, Germany.
The semantics of version control
Workshop on Realistic Program Verification. Nijmegen.
Datatype generic programming in F#
Workshop on Generic Programming. Vancouver, BC.
Auto in Agda
Mathematics of Program Construction. Königswinter, Germany.
Functional Programming in Swift
BOB Konf. Berlin.
The semantics of version control
Onward! '14. Portland, OR.
Auto in Agda
Brouwer Seminar. Nijmegen, the Netherlands.
Auto in Agda
IFIP WG 2.1 Meeting. Zeegse, the Netherlands.
The Semantics of Version Control
IFIP WG 2.1 Meeting. Schloss Reisensburg.
xmonad in Coq: programming a window manager in a proof assistant
Haskell Symposium. Copenhagen, Denmark.
Applications of reflection in Agda
Implementation and Applications of Functional Languages (IFL). Oxford, UK.
How I generate my homepage
Dutch HUG Day. Utrecht, the Netherlands.
From Mathematics to Abstract Machine
The Fourth Workshop on Mathematically Structured Functional Programming. Tallinn, Estonia.
A formal derivation of an executable Krivine machine
IFIP WG 2.1 Meeting. Rome, Italy.
xmonad in Coq: programming a window manager in a proof assistant
Dutch FP Day. Utrecht, the Netherlands.
From Math to Machine: A formal derivation of an executable Krivine machine
Brouwer Seminar. Nijmegen, the Netherlands.
Data types à la carte
Dutch HUG meeting. Utrecht, the Netherlands.
Dependently typed programming
Summer School on Applied Functional Programming. Utrecht, the Netherlands.
De programmeertaal van de toekomst
NWO Bessensap. Den Haag, the Netherlands.
Dependent types, predicate transformers, and refinement
IFIP WG 2.1 Meeting. Reykjavik, Iceland.
Adventures in Extraction
Brouwer Seminar. Nijmegen, the Netherlands.
An introduction to Agda
Brouwer Seminar. Nijmegen, the Netherlands.
Stream Fusion
Stream Seminar. Nijmegen, the Netherlands.
The Problem of the Dutch National Flag
IFIP WG 2.1 Meeting. Atlantic City, NJ.
The Logic of Interaction
Brouwer Seminar Series. Nijmegen, the Netherlands.
Me and my research
Vector Fabrics Technical Seminar. Eindhoven, the Netherlands.
The problem of the Dutch National Flag
Dutch FP Day. Nijmegen, the Netherlands.
The problem of the Dutch National Flag
Agda Implementors' Meeting. Göteborg, Sweden.
A Hoare Logic for the State Monad
TPHOLS 2009. München, Germany.
Chalk: A tool for architecture design
Chalmers FP Day. Göteborg, Sweden.
High level architectural modelling for early estimation of power and performance
Hardware design and Functional Languages. York, UK.
A functional specification of effects
Chalmers SET talk. Göteborg, Sweden.
Domain specific embedded languages
Given at the Ericsson DSL4DSP meeting. Göteborg, Sweden.
The Hoare State Monad
Dutch FP Day. Eindhoven, the Netherlands.
The Power of Pi
ICFP 2008. Victoria, BC.
Towards a functional specification of effects
University of Sussex. Brighton, UK.
The Power of Pi
Agda Implementors' Meeting. Göteborg, Sweden.
Dependent Types for Distributed Arrays
Trends in Functional Programming 2008. Heijen, the Netherlands.
The Power of Pi
TYPES Workshop on Dependently Typed Programming 2008. Nottingham, UK.
A total functional specification of mutable state
TYPES Workshop on Effects in Type Theory. Tallinn, Estonia.
Beauty in the Beast: A Functional Semantics of the Awkward Squad
Haskell Workshop 2007. Freiburg, Germany.
A Functional Specification of Effects
PhD Research Seminar. Leicester.
Implementing a Dependently Typed Lambda Calculus
Invited seminar at the University of Sheffield. Sheffield, UK.
I/O in a Dependently Typed Programming Language
TYPES 2007. Udine, Italy.
Implementing a Dependently Typed Lambda Calculus
Utrecht University Software Technology Colloquium. Utrecht, the Netherlands.
Compiler Correctness in Coq
Foundations of Programming Group Away Day. Ruddington, UK.
Implementing Observational Equality in Epigram 2
TYPES Workshop on Curry-Howard Implementation Techniques. Nijmegen, the Netherlands.
A Principled Approach to Version Control
Given at the first Fun in the Afternoon Meeting. Oxford, UK.
Dependable software development
Foundations of Programming research seminar. Nottingham, UK.
Better software with better types
Given at Microsoft Research. Redmond, USA.
Isomorphisms for context-free types
TYPES 2006. Nottingham, UK.
Isomorphisms for context-free types
BCTCS 2006. Swansea, UK.
Plug-and-play attribute grammars
AFP 2004 student sessions. Tartu, Estonia.