Thema3455: Unterschied zwischen den Versionen
Serge Stratan (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Abschlussarbeit |Titel DE=Towards a Categorical Semantics for the Open Calculus of Constructions |Titel EN=Towards a Categorical Semantics for the Open Calcu…“) |
Serge Stratan (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 8: | Zeile 8: | ||
|Forschungsgruppe=Wissensverarbeitung | |Forschungsgruppe=Wissensverarbeitung | ||
|Abschlussarbeitsstatus=Abgeschlossen | |Abschlussarbeitsstatus=Abgeschlossen | ||
|Abgabe=2007 | |Beginn=2007/03/13 | ||
|Abgabe=2007/03/13 | |||
|Ergebnisse=10.1.1.115.8966.pdf | |||
|Beschreibung DE=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. | |||
|Beschreibung EN=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. | |||
}} | }} | ||
Aktuelle Version vom 13. Dezember 2016, 22:53 Uhr
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.
