- Jesper Cockx,
Theory and implementation of Agda
- Since October 2017 employed on my project
Termination Certificates for Dependently-Typed Programs and Proofs via Refinement Types,
VR Grant 2014-4864.
Jesper's PhD thesis (2017) on Dependent Pattern Matching and Proof-Relevant Unification
won a distinction (congratulations of the jury)
from KU Leuven given to at most the top 5% PhD theses.
He further won
the 2017/18 EAPLS Best PhD Dissertation Award.
Supervised PhD students
- Víctor López Juan,
Implementing a Dependent Type-Checker with Implicit Arguments (ongoing)
- Co-supervision since 2015 (Chalmers); main supervisor: Nils Anders Danielsson.
- Andrea Vezzosi,
On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory (2018)
- PhD student (2014-2018) at Chalmers on my project Termination Certificates for Dependently-Typed Programs and Proofs via Refinement Types, VR Grant 2014-4864.
Defense: 5 September 2018
Opponent: Rasmus Ejlers Møgelberg.
Examiner: Thierry Coquand.
Andrea is continuing as postdoc in the Programming, Logic, and Semantics group (PLS) at ITU Copenhagen.
- Christoph-Simon Senjak†,
An Implementation of Deflate in Coq (2018)
- PhD student at the Chair of Theoretical Computer Science, Ludwig-Maximilians-University Munich (LMU).
I supervised Christoph-Simon 2012-2013.
After my transition to Gothenburg Martin Hofmann† took over, then Ulrich Schöpp.
He defended on 12 December 2018 with magna cum laude (mark 1.1).
He passed away on 4 January 2019.
- Dulma Rodriguez,
Amortised Resource Analysis for Object-Oriented Programs (2012)
- Martin Hofmann† was main, I was secondary supervisor (LMU, 2008-2012).
Dulma is now (2019) software engineer at Facebook in London.
Supervised Master's Theses
Ongoing supervisions (2019):
- Elias Forsberg, A Formally Verified Parser Generator in Agda
- Alexander Fuhs, Verified Compilation of an Intrinsically-Typed WHILE Language in Agda
- Siavash Hamedani, Agda's Scope Checker implemented in Agda
- Jannis Limperg, Modeling Agda’s Sized Types in Agda
- Frederik Folkmar Ramcke, LF Definability in Agda
A master's thesis amounts to 6 man months full-time work.
- Pierre Krafft, Singly Typed Actors in Agda (2018)
Formalization of typed actors with selective receive.
Examiner: Mary Sheeran.
Agda code on github
- Joakim Öhman,
A Logical Relation for Dependent Type Theory Formalized in Agda
- co-supervision with Andrea Vezzosi
Agda code: on github
Publication: Decidability of Conversion for Type Theory in Type Theory
Joakim is now (2019) pursuing a PhD under the supervision of Aleksander Nanevski at IMDEA, Madrid, Spain.
- Glen Mevel, On System U with eta-equality (Mar-Aug 2016)
- 5-month ENS Cachan internship.
- Theo Winterhalter, Computationally Irrelevant Sizes in Dependent Type Theory (Mar-Aug 2015)
- 5-month ENS Cachan internship.
TYPES 2016 abstract
ICFP 2017 paper
Theo is now (2019) pursuing a PhD under the supervision of Nicolas Tabareau at the University of Nantes, France.
- Marcus Eskil Johansson and Jesper Lloyd, Eliminating the problems of hidden-lambda insertion (2015)
- Restricting implicit arguments for increased predictability of type checking
in a functional programming language with dependent types.
- Matthias Benkard, Type Checking without Types (2012)
- Investigation of a functional language
with pattern matching and a refinement
relation between terms that plays the role of typing and
Won a ICFP 2012 Student research competition travel award
and a 10min presentation at the main conference.
ICFP 2012 Poster,
- Frederic Kettelhoit, A Prelude for Agda (2011/12)
- Design of a prelude for the Agda standard library,
based on type classes for overloaded identifiers.
Agda Prelude auf Github
- Gabriel Scherer,
Universe Subtyping in Martin-Löf Type Theory (Apr-Aug 2011)
- Construction of a Kripke model for dependent type theory with a predicative cumulative universe hierarchy.
Conducted as 5-month ENS internship on the level of a Master's thesis.
Gabriel is now (2019) a permanent researcher in the Parsifal team of INRIA Saclay, France.
- Karl Mehltretter,
Termination Checking for a Dependently Typed Language (2007)
- A Haskell implementation of a core dependently typed language with sized types and recursive and corecursive functions. Every well-typed program is terminating.
- Dulma Rodriguez,
Algorithmic Subtyping for Higher-Order Bounded Quantification Revisited (2007)
- A much simplified proof of decidability of Fω<:. The subtyping algorithm uses long normal forms and
publication at CSL 2008
Supervised Student Research Projects and Bachelor's Theses
A student project or bachelor's thesis amounts to 3 man months full-time work.
- Gregor Ulm, Compiling Agda to Fω (Aug 2014 - May 2015)
- A study on type-based program extraction.
Gregor is now (2019) working for the Fraunhofer-Chalmers Centre for Industrial Mathematics.
- Felix Reihl, Solving Size Constraints Using Graph Representation
(Feb - Aug 2013)
- A solver for simple inequality constraints under hypotheses.
Terms range over the natural numbers plus infinite,
with maximum and increment as operations.
- David Thibodeau,
A Core Calculus for Covering Copatterns
(May - Aug 2012)
- A simply-typed calculus to define infinite objects by observations.
Syntactic proof of type soundness: type preservation and progress.
Preliminary technical report
publication at POPL 2013
David is now (2019) PhD student under supervision of Brigitte Pientka at McGill University, Montreal, Canada.
- Nicolai Kraus, A Lambda Term Representation Based on Ordered Linear Logic (2010/11)
- HELF: Haskell implementation of a new term representation for type checking the Edinburgh Logical Framework (LF). Experimental comparison with an implementation of β-normal terms based on hereditary substitutions.
publication at LFMTP 2011
Nicolai continued to do a PhD under the supervision of Thorsten Altenkirch at the University of Nottingham. His thesis won the Ackermann Award 2016. He is now (2019) research fellow at the University of Nottingham.
- Julien Oster, Red-Black Trees with Static Representation Invariants (2009/10)
- A dependently-typed implementation of red-black trees in Agda. Search-tree invariant and balancing are ensured by type checking.
Julien is now (2019) OS Developer at Apple, Cupertino, CA, USA.
- Jan Peter Gutzmann, Implementation of a Type Checker for System Fω (2003)
- A Haskell implementation for checking fully-annotated (Church-style) definitions in the higher-order polymorphic λ-calculus. See page church.
Bor-Yuh Evan Chang,
Human-reable machine-verifiable proofs for teaching constructive logic (2001)
- Design of an extension of the tutorial proof checker tutch to handle bigger proof steps. Presented at the workshop PTP-01, IJCAR 2001, Siena, Italy.
Evan is now (2019) associate professor in the Programming Languages and Verification group at University of Colorado Boulder.
Supervised Industrial Master's Theses
- Alaa Alnuweiri and Jemima Masamu,
Generic Log and Performance Data from Customer Installations
- with Ascom (2016)
- Philip Dahlstedt and Gustav Öhman,
Dynamic and fault tolerant distributed computations using the actor model
- with Syntronic Research and Development AB (2016)
- Anton Lindgren,
Low-latency floating subsets through combined indexes
- with Yolean (2016)
Supervised Bachelor's Theses Carried Out as Group Projects
Group (4-6 members) projects proposed by me:
- A Smartphone Game Modeled after Logic and Proofs
- Jonatan Källman, Elias Wållberg Burström, Felix Nordén, Tuyen Ngo (ongoing)
- Exploring the Concept of Abstracting and Visualizing Formal Logic Proofs in Games Development and Evaluation of Gentzen’s Quest
- Johannes Backlund, Ludvig Ekman, Magnus Harryson, Johan Ronnås, Robin Åstedt, Jonatan Öberg.
Implementing and evaluating a smartphone game for playful introduction to natural deduction for propositional logic.
Android game Gentzen's Quest on Google Play
Video of presentation
Supervised Student-Proposed Bachelor's Theses
Students of DAT (Data- och informationsteknik) at Chalmers/GU proposed
and carried out the following bachelor theses under my supervision:
- Making and Acting on Predictions in StarCraft Brood War
Henrik Alburg, Filip Brynfors, Björn Persson Mattsson,
Florian Minges, Jakob Svensson. Improvement of the AI of the UAlbertaBot. (2014)
- Safe and Social: Location-based Social Networking Focusing on Security
- Julia Gustafsson, Antonious Kioksoglou, Anton Kloek, Victor Lindhé, Barnabas Sapan.
Android App with encrypted communication to a server with an encrypted database. (2014)
- Generation of music through genetic algorithms
- Viktor Anderling, Olle Andreasson, Christoffer Olsson, Sean Pavlov, Christian Svensson, Johannes Wikner. An attempt to apply evolutionary theory to MIDI-files. (2014)
The border between music and noise is always culturally defined.
(Jean-Jacques Nattiez, Music and discourse: Toward a semiology of music. Princeton, 1990. p.48)
- A general peer-to-peer based distributed computation network
- Jack Petterson, Leif Schelin, Niklas Wärvik, Joakim Öhman.
Like SETI@home, but fully decentralized. (2014)
| Professional Service