Teaching

My Courses

• Computer-Aided Formal Reasoning: Rechnergestütztes Beweisen (2010/11)
• Lambda-Calculus:
  • Lambda-Kalkül (2008/09)
  • Lambda-Kalkül (2006/07)
• Python Tutorial: Python-Kompaktkurs (2008/09)
• Theory and Implementation of Object-Oriented Programming Languages: Theorie und Implementation objekt-orientierter Programmiersprachen (2002)

My Shared Courses

• Compiler Construction Lab:
  • Compilerbau (2011/12) with Ulrich Schöpp
  • Übersetzerbaupraktikum (2007/08) with Hans-Wolfgang Loidl
• Type Systems:
  • Typsysteme (2011) with Ulrich Schöpp
  • Typsysteme (2007) with Martin Hofmann
• Semantics of Programming Languages: Semantik von Programmiersprachen (2010) with Ulrich Schöpp
• Advanced Functional Programming: Funktionale Programmierung (2009) with Hans-Wolfgang Loidl
• Computer-Aided Formal Reasoning: Rechnergestütztes Beweisen (2007/08) with Martin Hofmann

Seminars

• Scientific Practices: Wissenschaftliches Arbeiten und Lehren (2011) by Martin Hofmann
• Distributed Algorithms: Blockseminar Verteilte Algorithmen (2010) with Martin Hofmann and Ulrich Schöpp
• Programming Language Theory: Hauptseminar Programmiersprachentheorie (2007) with Lennart Beringer and Hans-Wolfgang Loidl

Assistance

• Algorithms and Data Structures:
  • Algorithmen und Datenstrukturen (2009) by Martin Hofmann
  • Effiziente Algorithmen (2006) by Martin Hofmann
  • Effiziente Algorithmen by Martin Hofmann and Jan Johannsen
• Functional Programming in SML: Programmierung und Modellierung (2008) by Francois Bry
• Constructive Logic (2000) by Frank Pfenning

Supervision

Supervised Master's Theses

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 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

Supervised Student Projects and Bachelor's Theses

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

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

Andreas Abel, http://www.tcs.ifi.lmu.de/~abel Last modified: Tue Nov 18 10:48:06 CET 2008