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
Difunctorial Semantics of Object Calculus
Stockholm University, Faculty of Science, Numerical Analysis and Computer Science(NADA) (together with KTH).
2005 In: Electronic Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 138, no 2, 79-94 p.Article in journal (Refereed) Published
Place, publisher, year, edition, pages
2005. Vol. 138, no 2, 79-94 p.
Identifiers
URN: urn:nbn:se:su:diva-24595OAI: oai:DiVA.org:su-24595DiVA: diva2:197857
Note
Part of urn:nbn:se:su:diva-7208Available from: 2007-12-04 Created: 2007-12-03Bibliographically approved
In thesis
1. Primitive Direcursion and Difunctorial Semantics of Typed Object Calculus
Open this publication in new window or tab >>Primitive Direcursion and Difunctorial Semantics of Typed Object Calculus
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
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:nbn:se:su:diva-7208 (URN)978-91-7155-550-2 (ISBN)
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

Open Access in DiVA

No full text

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

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 33 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