Towards a Categorical Semantics for the Open Calculus of Constructions

Master's thesis by Max Schäfer

Supervisor Steffen Hölldobler
Wissensverarbeitung
13 März 2007 – 13 März 2007
Download

Stehr’s Open Calculus of Constructions combines a type theory in

the style of the Calculus of Constructions with concepts from rewriting logic. Stehr’s original thesis gives a very simple set-theoretic semantics for the calculus, which abstracts away many of its more peculiar features, and is mainly used to obtain a semantic consistency proof. We present a more sophisticated, categorical semantics in the tradition of Streicher and Jacobs for a restricted variant of Stehr’s original system. Specifi- cally, we show that rewriting can be modelled by enriching the traditional, (1-)categorical approach with a 2-category structure, much in the spirit of Meseguer’s 2-functorial semantics for rewriting logic. The semantics thus obtained is a good match for the system under consideration, as witnessed by a soundness proof, and could serve as a basis for further investigations into the meta-theoretic properties of related systems.