Supervision

Postdoc

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.
Committee: Robert Atkey, Hugo Herbelin, Andrew Pitts.
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

Pierre Krafft, Singly Typed Actors in Agda (2018): Formalization of typed actors with selective receive. Examiner: Mary Sheeran.
Agda code on github Thesis
Joakim Öhman, A Logical Relation for Dependent Type Theory Formalized in Agda (Apr-Nov 2016): co-supervision with Andrea Vezzosi
Agda code: on github Publication: Decidability of Conversion for Type Theory in Type Theory POPL 2018

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 subtyping.
Won a ICFP 2012 Student research competition travel award and a 10min presentation at the main conference.
ICFP 2012 Poster, TCS Oberseminar-Vortrag
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.
Report LMCS article

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.
thesis slides Haskell code MiniAgda homepage
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 hereditary substitutions.
thesis slides publication at CSL 2008

A master's thesis amounts to 6 man months full-time work.

Supervised Student Research Projects and Bachelor's Theses

Gregor Ulm, Compiling Agda to Fω (Aug 2014 - May 2015): A study on type-based program extraction. Bachelor Thesis

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. Bachelor Thesis.
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.
HELF source 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.
RBTree source Draft paper Slides

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.

A student project or bachelor's thesis amounts to 3 man months full-time work.

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. (2018)
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)

Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: 2019-01-22 17:50