Talks
- Programming with dependent types: beyond evaluating the simply typed lambda calculus
- IFL invited talk. Nijmegen, the Netherlands.
- The functional essence of imperative binary search trees
- IFIP WG 2.8. Utrecht, the Netherlands.
- A correct by construction conversion to combinators
- IFIP WG 2.8. Utrecht, the Netherlands.
- The functional essence of imperative binary search trees
- IFIP WG 2.1. Neustadt an der Weinstraße, Germany.
- 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.
- Correct by construction conversion to combinators
- Agda Implementors Meeting. Delft.
- Purely functional, fully in-place programming
- Algorithms Seminar. Utrecht.
- Calculating datastructures
- Dutch FP Day. Eindhoven.
- 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.
