A Type-Based Approach to Component-Oriented Synthesis

Jakob Rehof (Technische Universität Dortmund).

Course Summary | About the lecturer | Location and schedule | Materials | Assignment

Course summary: The synthesis problem (given a logical specification, to construct a program satisfying the specification) is one of the most challenging problems in computer science. The problem is intrinsically of high computational complexity. Moreover, a no less important problem from a pragmatic perspective is the challenge of specification complexity – how to allow for adequate specifications that can be naturally connected to code without requiring unrealistic human effort. One recent line of approaches towards meeting these challenges is to consider synthesis as a component-based problem, that is, as a problem of program composition from a collection (“repository”) of components which may embody human design intelligence (rather than as a problem of synthesis “from scratch”). Our approach (“Combinatory Logic Synthesis”, CLS) is based on the theory of inhabitation (is there a term having a given type?) in combinatory logic with intersection types which are used to specify components semantically. In this course we will present an overview of both the theoretical foundations of CLS as well as applications of CLS within a framework implemented as a language extension to the programming language Scala.

About the lecturer: Since 2006 Jakob Rehof holds a joint position as full professor of Computer Science at the University of Dortmund, where he is chair of Software Engineering, and as a director of the Fraunhofer-Institute for Software and Systems Engineering (ISST) in Dortmund. Jakob Rehof studied Computer Science and Mathematics at the University of Copenhagen and got his Ph.D. in Computer Science at DIKU, Department of Computer Science, University of Copenhagen. In 1997 Rehof was a visiting Researcher at the University of Stanford, CA, USA. From 1998 until 2006 he was at Microsoft Research, Redmond, WA, USA. Prior to all of the above he studied Classical Philology (Latin & Greek) and Philosophy at the University of Aarhus and the University of Copenhagen and was a DAAD scholar at the Eberhard-Karls University of Tübingen.

Location and schedule: Rooms 5070 and 2180 in MIMUW building.

Friday, December 1st, Room 5070
14:15 - 15:45 lecture
15:45 - 16:00 coffee and cake
16:00 - 17:00 class
17:00 - 17:15 coffee and cake
17:15 - 18:00 lecture
Saturday, December 2nd, Room 2180
10:00 - 10:45 lecture
10:45 - 11:00 coffee and cake
11:00 - 12:00 class
12:00 - 12:30 lunch for registered participants
12:30 - 14:00 lecture
14:00 - 14:15 coffee and cake
14:15 - 15:00 class

Materials
Lecture 0: Lecture Overview
Lecture 1: Typed λ-calculus and Combinatory Logic
Lecture 2: Inhabitation in Simple Types
Lecture 3: Inhabitation in Intersection Types and Bounded Combinatory Logic
Lecture 4: The CLS Framework
Lecture 5: Dimensional Intersection Type Calculus

Coq verification of the two counter proof

Classes:
Combinatory Logic and Two Counter Automata
Subtyping and Type Derivation
Combinator Implementation in Scala


Assignment: problem set. Please submit the solutions at the address Jakob.Rehof@tu-dortmund.de by January 29th.