Mathematisches Kolloquium

Zusammenfassung: The most popular today proof assistant Coq is based on a formal reasoning system CIC which belongs to the class of the so called Martin-Lof type systems. Despite it popularity in computer science, Coq has not been widely used by the mathematical community in part because no natural classical model for Martin-Lof type systems have been known. In my talk I will outline a construction of such a model.

This model is, up to an appropriate equivalence, the only one satisfying what I call the equivalence axiom and therefore provides a completely canonical (classical) semantics for Martin-Lof type systems. The name "homotopy lambda calculus" in the title refers to the new reasoning system which one obtains by allowing arbitrary extensions of the core type system which are compatible with the canonical model.

Alle Interessierten sind hiermit herzlich eingeladen. Eine halbe Stunde vor dem Vortrag gibt es Kaffee und Tee vor dem Hörsaal B006.

Treffpunkt zum Abendessen um 18.00 Uhr wird noch bekannt gegeben.