Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Primitive Direcursion and Difunctorial Semantics of Typed Object Calculus
Stockholm University, Faculty of Science, Numerical Analysis and Computer Science(NADA) (together with KTH).
2007 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In the first part of this thesis, we contribute to the semantics of typed object calculus by giving (a) a category-theoretic denotational semantics using partial maps making use of an algebraic compactness assumption, (b) a notion of "wrappers'' by which algebraic datatypes can be represented as object types, and (c) proofs of computational soundness and adequacy of typed object calculus via Plotkin's FPC (with lazy operational semantics), thus making models of FPC suitable also for first-order typed object calculus (with recursive objects supporting method update, but not subtyping). It follows that a valid equation in the model induces operationally congruent terms in the language, so that program algebras can be studied. For (c), we also develop an extended first-order typed object calculus, and prove subject reduction. The second part of the thesis concerns recursion principles on datatypes including the untyped lambda calculus as a special case. Freyd showed that in certain domain theoretic categories, locally continuous functors have minimal invariants, which possess a structure that he termed dialgebra. This gives rise to a category of dialgebras and homomorphisms, where the minimal invariants are initial, inducing a powerful recursion scheme (direcursion) on a complete partial order. We identify a problem that appears when we translate (co)iterative functions to direcursion, and as a solution to this problem we develop a recursion scheme (primitive direcursion). This immediately gives a number of examples of direcursive functions, improving on the situation in the literature where only a few examples have appeared. By means of a case study, this line of work is connected to object calculus models.

Place, publisher, year, edition, pages
Stockholm: Numerisk analys och datalogi (NADA), (tills m KTH) , 2007. , 185 p.
Series
Trita-CSC-A, ISSN 1653-5723 ; 22
Keyword [en]
denotational semantics, axiomatic domain theory, coalgebra, primitive (co)recursion, object-based programming, typed object calculus
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:su:diva-7208ISBN: 978-91-7155-550-2 (print)OAI: oai:DiVA.org:su-7208DiVA: diva2:197860
Public defence
2008-01-09, Lecture Theatre F3, Royal Institute of Technology, Lindstedtsvägen 26, Stockholm, 14:00
Opponent
Supervisors
Note
Delarbete II är även publicerad som Teknisk rapport, 2007, Oct, No2.Available from: 2007-12-04 Created: 2007-12-03Bibliographically approved
List of papers
1. Difunctorial Semantics of Object Calculus
Open this publication in new window or tab >>Difunctorial Semantics of Object Calculus
2005 In: Electronic Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 138, no 2, 79-94 p.Article in journal (Refereed) Published
Identifiers
urn:nbn:se:su:diva-24595 (URN)
Note
Part of urn:nbn:se:su:diva-7208Available from: 2007-12-04 Created: 2007-12-03Bibliographically approved
2. Computational Soundness and Adequacy for Typed Object Calculus
Open this publication in new window or tab >>Computational Soundness and Adequacy for Typed Object Calculus
2008 In: International Workshop on Foundations of Object-Oriented Languages (FOOL 2008, co-located with POPL 2008), ACM SIGPLAN, Vol. Jan.Article in journal (Refereed) Published
Identifiers
urn:nbn:se:su:diva-24596 (URN)
Note
Part of urn:nbn:se:su:diva-7208Available from: 2007-12-04 Created: 2007-12-03Bibliographically approved
3. Parametric (Co)Iteration vs. Primitive Direcursion
Open this publication in new window or tab >>Parametric (Co)Iteration vs. Primitive Direcursion
2007 In: Algebra and Coalgebra in Computer Science: Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007. Proceedings, 2007, 257-278 p.Chapter in book (Other academic) Published
Identifiers
urn:nbn:se:su:diva-24597 (URN)
Note
Part of urn:nbn:se:su:diva-7208Available from: 2007-12-04 Created: 2007-12-03Bibliographically approved

Open Access in DiVA

fulltext(1379 kB)385 downloads
File information
File name FULLTEXT01.pdfFile size 1379 kBChecksum SHA-1
e131a2350124201331bc294066fef3f888db15da366d574b27179fefb4fda05232684176
Type fulltextMimetype application/pdf

By organisation
Numerical Analysis and Computer Science(NADA) (together with KTH)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 385 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 970 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf