Teaching

Type Systems (Typsysteme), with Martin Hofmann, Summer 2007, LMU, Munich.

• concept and lecture with Martin (each 2 hours * 14 weeks)
• tutorial section (2 hour * 14 weeks)
• design and grading of assignments

Programming Language Theory, seminar, (Hauptseminar Programmiersprachentheorie) with Lennart Beringer and Hans-Wolfgang Loidl, Summer 2007, LMU, Munich.

• concept and seminar (2 hours * 8 weeks)

Lambda-Calculus (Lambda-Kalkül), Winter 2006/07, LMU, Munich.

• concept and lecture (3 hours * 14 weeks)
• tutorial section (1 hour * 14 weeks)
• design and grading of assignments
• oral exam

Efficient Algorithms (Effiziente Algorithmen) by Martin Hofmann, Summer 2006, LMU, Munich.

• design of assignments
• tutorial section (2 hours * 14 weeks)
• grading of assignments

Computer-Aided Formal Reasoning (Rechnergestütztes Beweisen) by Martin Hofmann, Winter 2005/06, LMU, Munich.

• tutorial section (2 hours * 14 weeks)
• design and grading of assignments

Compiler Construction Lab (Übersetzerbaupraktikum) by Martin Hofmann, Winter 2005/06, LMU, Munich.

• tutorial section (4 hours * 14 weeks)

Theory and Implementation of Object-Oriented Programming Languages (Theorie und Implementation objekt-orientierter Programmiersprachen), Summer 2002, LMU, Munich.

• concept and lecture (2 hours * 14 weeks)
• tutorial section (2 hours * 14 weeks)
• design and grading of assignments
• oral exam resp. student project

Efficient Algorithms (Effiziente Algorithmen) by Martin Hofmann and Jan Johannsen, Summer 2002, LMU, Munich.

• tutorial section
• grading of assignments

Constructive Logic (15-399) by Frank Pfenning, Fall 2000, CMU, Pittsburgh.

• development and maintenance of the proof checker tutch
• tutorial section
• design and grading of assignments

Theoretical Computer Science (Einführung in die Informatik IV) by Fred Kröger, Summer 1998, LMU, Munich.

• tutorial section
• grading of assignments

Theoretical Computer Science (Einführung in die Informatik IV) by Peter Clote, Summer 1997, LMU, Munich.

• grading of assignments

Supervised Master's Theses

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

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

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 | Personal page ]

Andreas Abel, http://www.tcs.informatik.uni-muenchen.de/~abel Last modified: Tue Jul 24 18:22:00 CEST 2007