Löw, Tobias (2007)
Locally Boolean Domains and Universal Models for Infinitary Sequential Languages.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung
Kurzbeschreibung (Abstract)
In the first part of this Thesis we develop the theory of locally boolean domains and bistable maps and show that the category of locally boolean domains and bistable maps is equivalent to the category of Curien-Lamarche games and observably sequential functions. Further we show that the category of locally boolean domains has inverse limits of ω-chains of embedding/projection pairs. In the second part we consider the category of locally boolean domains and bistable maps as model for functional programming languages: in "Bistable biorders: a sequential domain theory" J. Laird has shown that an infinitary sequential extension of the functional core language PCF has a fully abstract model in the category of locally boolean domains. We introduce an extension SPCF∞ of his language by recursive types and show that it is universal for its model in locally boolean domains. Finally we consider an infinitary target language CPS∞ for the CPS translation presented by B. Reus and T. Streicher in "Classical logic, continuation semantics and abstract machines" and show that it is universal for a model in locally boolean domains which is constructed like Dana Scott's D∞ where D = O = {⊥,⊤}.
Typ des Eintrags: |
Dissertation
|
Erschienen: |
2007 |
Autor(en): |
Löw, Tobias |
Art des Eintrags: |
Erstveröffentlichung |
Titel: |
Locally Boolean Domains and Universal Models for Infinitary Sequential Languages |
Sprache: |
Englisch |
Referenten: |
Streicher, Prof. Dr. Thomas ; Laird, Dr. James David |
Berater: |
Streicher, Prof. Dr. Thomas |
Publikationsjahr: |
1 März 2007 |
Ort: |
Darmstadt |
Verlag: |
Technische Universität |
Datum der mündlichen Prüfung: |
1 Dezember 2006 |
URL / URN: |
urn:nbn:de:tuda-tuprints-7902 |
Kurzbeschreibung (Abstract): |
In the first part of this Thesis we develop the theory of locally boolean domains and bistable maps and show that the category of locally boolean domains and bistable maps is equivalent to the category of Curien-Lamarche games and observably sequential functions. Further we show that the category of locally boolean domains has inverse limits of ω-chains of embedding/projection pairs. In the second part we consider the category of locally boolean domains and bistable maps as model for functional programming languages: in "Bistable biorders: a sequential domain theory" J. Laird has shown that an infinitary sequential extension of the functional core language PCF has a fully abstract model in the category of locally boolean domains. We introduce an extension SPCF∞ of his language by recursive types and show that it is universal for its model in locally boolean domains. Finally we consider an infinitary target language CPS∞ for the CPS translation presented by B. Reus and T. Streicher in "Classical logic, continuation semantics and abstract machines" and show that it is universal for a model in locally boolean domains which is constructed like Dana Scott's D∞ where D = O = {⊥,⊤}. |
Alternatives oder übersetztes Abstract: |
Alternatives Abstract | Sprache |
---|
Im ersten Teil dieser Arbeit wird die Theorie lokal boolescher Bereiche und bistabiler Abbildungen entwickelt. Es wird gezeigt, dass die Kategorie lokal boolescher Bereiche und bistabiler Abbildungen zur Kategorie von Curien-Lamarche Spielen und beobachtbar sequenzieller Funktionen äquivalent ist. Weiterhin zeigen wir, dass die Kategorie lokal boolescher Bereiche und bistabiler Abbildungen inverse Limiten von ω-Ketten von Einbettungs-/Projektionspaaren besitzt. Im zweiten Teil der Arbeit betrachten wir die Kategorie lokal boolescher Bereiche und bistabiler Abbildungen als Modell für funktionale Programmiersprachen: in "Bistable biorders: a sequential domain theory" hat J. Laird gezeigt, dass es in der Kategorie lokal boolescher Bereiche ein voll abstraktes Modell für eine infinitäre, sequentielle Erweiterung der funktionalen Kernsprache PCF gibt. Wir definieren SPCF∞, eine Erweiterung von Lairds Sprache um rekursive Typen, und zeigen, dass diese Sprache universell bezüglich ihres Modells in der Kategorie lokal boolescher Bereiche ist. Schließlich betrachten wir eine infinitäre Zielsprache CPS∞ für die CPS Übersetzung aus "Classical logic, continuation semantics and abstract machines" von B. Reus and T. Streicher und zeigen, dass sie universell bezüglich ihres Modells in der Kategorie lokal boolescher Bereiche ist, welches wie Dana Scotts D∞ mit D = O = {⊥,⊤} konstruiert ist. | Deutsch |
|
Sachgruppe der Dewey Dezimalklassifikatin (DDC): |
500 Naturwissenschaften und Mathematik > 510 Mathematik |
Fachbereich(e)/-gebiet(e): |
04 Fachbereich Mathematik |
Hinterlegungsdatum: |
17 Okt 2008 09:22 |
Letzte Änderung: |
26 Aug 2018 21:25 |
PPN: |
|
Referenten: |
Streicher, Prof. Dr. Thomas ; Laird, Dr. James David |
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: |
1 Dezember 2006 |
Export: |
|
Suche nach Titel in: |
TUfind oder in Google |
|
Frage zum Eintrag |
Optionen (nur für Redakteure)
|
Redaktionelle Details anzeigen |