Teaching
Summer Schools
 Agda Tutorial
 Autumn school Proof and Computation for graduate and PhD students and young PostDocs.
38 October 2016, Aurachhof, Fischbachau, Bayern, Germany
Tutorial material for live coding:
Prelude.agda
TreeSortBool.agda
TreeSortOrd.agda
Copatterns.agda
Solutions:
TreeSortOrdSolution.agda
CopatternsSolution.agda
Solutions pretty:
TreeSortOrdSolution.html
CopatternsSolution.html
 Type Theory. A Constructive Foundation for Logics and Computer Science
 28th European Summer School in Logic, Language and Information (ESSLLI 2016)
BolzanoBozen, South Tyrol, Italy, 1526 August 2016
Introductory course: Type Theory. A Constructive Foundation for Logics and Computer Science
(local copy)
My Courses
 Programming Language Technology (Master level):
 Logic, Algorithms, and Data Structures (Bachelor level):
 ComputerAided Formal Reasoning:
 LambdaCalculus (Skript)
 Python Tutorial (Folien)
 Theory and Implementation of ObjectOriented Programming Languages
(Skript)
My Shared Courses
 Advanced Functional Programming
(Folien: Haskell Agda)
 Compiler Construction Lab:
 Functional Programming in SML:
 Type Systems:
 Semantics of Programming Languages:
 ComputerAided Formal Reasoning:
Seminars
Assistance
Detailed listing of my teaching until 2011...
Supervision
Supervised PhD students
 Andrea Vezzosi,
Sized and Guarded Dependent Types
 Supervision since 2014 (Chalmers).
 Víctor López Juan,
Parametrized Modules for Dependent Types
 Supervision since 2015 (Chalmers).
 ChristophSimon Senjak,
Verification of Deflate (RCF 1951)
 I supervised ChristophSimon 20122013 (LMU).
 Dulma Rodriguez,
Amortised Resource Analysis for ObjectOriented Programs (2012)
 Martin Hofmann was main, I was secondary supervisor (LMU, 20082012).
Dulma is now software engineer at Facebook in London.
Supervised Master's Theses
 Joakim Öhman, A Logical Relation for Dependent Type
Theory Formalized in Agda
(AprNov 2016)
 cosupervision with Andrea Vezzosi
Agda code: on github
 Glen Mevel, On System U with etaequality (MarAug 2016)
 5month ENS Cachan internship.
 Theo Winterhalter, Computationally Irrelevant Sizes in Dependent Type Theory (MarAug 2015)
 5month ENS Cachan internship.
 Marcus Eskil Johansson and Jesper Lloyd, Eliminating the problems of hiddenlambda 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 OberseminarVortrag
 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 MartinLöf Type Theory (AprAug 2011)
 Construction of a Kripke model for dependent type theory with a predicative cumulative universe hierarchy.
Report of this 5month ENS internship on the level of a Master's thesis.
 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 welltyped program is terminating.
thesis
slides
Haskell code
MiniAgda homepage
 Dulma Rodriguez,
Algorithmic Subtyping for HigherOrder Bounded Quantification Revisited (2007)
 A much simplified proof of decidability of Fω_{<:}. The subtyping algorithm uses long normal forms and
hereditary substitutions.
thesis
slides
A master's thesis amounts to 6 man months fulltime work.
Supervised Student Research Projects and Bachelor's Theses
 Gregor Ulm, Compiling Agda to Fω (Aug 2014  May 2015)
 A study on typebased program extraction.
Bachelor Thesis
 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 simplytyped calculus to define infinite objects by observations.
Syntactic proof of type soundness: type preservation and progress.
Preliminary technical report.
 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
 Julien Oster, RedBlack Trees with Static Representation Invariants (2009/10)
 A dependentlytyped implementation of redblack trees in Agda. Searchtree invariant and balancing are ensured by type checking.
RBTree source
 Jan Peter Gutzmann, Implementation of a Type Checker for System F_{ω} (2003)
 A Haskell implementation for checking fullyannotated (Churchstyle) definitions in the higherorder polymorphic λcalculus. See church home page.
 BorYuh Evan Chang,
Humanreable machineverifiable 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 PTP01, IJCAR 2001, Siena, Italy. (See also publications page.)
A student project or bachelor's thesis amounts to 3 man months fulltime work.
Supervised Industrial Master's Theses
 Alaa Alnuweiri and Jemima Masamu,
Generic Log and Performance Data from Customer Installations
 with Ascom
 Philip Dahlstedt and Gustav Öhman,
Dynamic and fault tolerant distributed computations using the actor model
 with Syntronic Research and Development AB
 Anton Lindgren,
Lowlatency floating subsets through combined indexes
 with Yolean
Supervised StudentProposed 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.
 Safe and Social: Locationbased 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.
 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 MIDIfiles.
The border between music and noise is always culturally defined
(JeanJacques Nattiez, Music and discourse: Toward a semiology of music. Princeton, 1990. p.48)
 A general peertopeer based distributed computation network
 Jack Petterson, Leif Schelin, Niklas Wärvik, Joakim Öhman.
Like SETI@home, but fully decentralized.
[ Home
 CV
 Projects
 Publications
 Talks
 Teaching
 Sharing
]
