Summer Schools (and similar courses)

Type Theory
5 lectures for CM0859, EAFIT University, Medellin, Colombia, 6-10 March 2017.
Agda Tutorial
Autumn school Proof and Computation for graduate and PhD students and young PostDocs.
Aurachhof, Fischbachau, Bayern, Germany, 3-8 October 2016.

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)
Bolzano-Bozen, South Tyrol, Italy, 15-26 August 2016
Introductory course: Type Theory. A Constructive Foundation for Logics and Computer Science (local copy)

My Courses

My Shared Courses



Detailed listing of my teaching until 2011...



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).
Christoph-Simon Senjak, Verification of Deflate (RCF 1951)
I supervised Christoph-Simon 2012-2013 (LMU).
Dulma Rodriguez, Amortised Resource Analysis for Object-Oriented Programs (2012)
Martin Hofmann was main, I was secondary supervisor (LMU, 2008-2012).
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 (Apr-Nov 2016)
co-supervision with Andrea Vezzosi
Agda code: on github
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.
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. Report of this 5-month 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 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
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
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.
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, 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
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 church home page.
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. (See also publications page.)
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 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)


[ Home | CV | Projects | Publications | Talks | Teaching | Sharing ]

Valid HTML 4.01! Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: 2017-04-28 21:24>
Valid CSS!