**(C) Ralf LĂ¤mmel, Andrei Varanovich, University of Koblenz Landau**

# Logistics

- Course site
- Date published: 5 Dec 2012
- Deadline SVN: 11 Dec 2012 (End of Day)
- SVN: https://svn.uni-koblenz.de/softlang/main/courses/plt1213/students + group name
- Present your solution with your own system.
- Lab assistant calls up teams.

# Assignment

You can use either typed, applied lambda calculus from the lecture or the untyped, applied lambda calculus from the previous assignment as the starting point for the present assignment. (The disadvantage of the lecture's calculus is that it may be harder to understand because it is so highly modularized.)

## Add types to the applied, untyped lambda calculus

You only need to do this part, if you start from the untyped calculus. (That is, you can skip this warm-up, if you start from the typed calculus that was presented in the lecture.)

## Addition of lists to the typed, applied lambda calculus

You need to support the following syntax, i.e., operations:

- nil: construction of the empty list.
- cons: construction of the nonempty list from a head value and a tail list.
- null: test for checking whether a given list is empty.
- head: retrieval of the head of a non-empty list.
- tail: retrieval of the tail of a non-empty list.

You need to add evaluation and typing rules for these list constructs. Of course, you also need dedicated type expressions to deal with lists of different element types. Further, you also need to extend the predicates for substitution and normal forms.

## Addition of n-tuples to the typed, applied lambda calculus

You should inspire yourself with the discussion of pairs from the lecture.

You need to support the following syntax, i.e., operations:

- Construction of n-tuples, i.e., tuples of arbitrary length.
- Projection of a n-tuple to a given index.

You need to add evaluation and typing rules for these tuple constructs. Of course, you also need dedicated type expressions to deal with tuples with different component types. Further, you also need to extend the predicates for substitution and normal forms.

## Explanation of the deeper difference between lists and n-tuples

This is just about a good explanation. You would refer to the type system and the semantics in some useful, deep way to make everyone understand differences and commonalities of lists and tuples.