Towards a Categorical Semantics for the Open Calculus of Constructions
Towards a Categorical Semantics for the Open Calculus of Constructions
Masterarbeit von Max Schäfer
- Betreuer Steffen Hölldobler
- Wissensverarbeitung
- 13. März 2007 – 13. März 2007
- Download
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.
