A Generic Type System for Higher-Order Ψ-calculi

Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt

Standard

A Generic Type System for Higher-Order Ψ-calculi. / Bendixen, Alex Rønning; Bojesen, Bjarke Bredow; Hüttel, Hans; Lybech, Stian.

I: Electronic Proceedings in Theoretical Computer Science, EPTCS, Bind 368, 2022, s. 43-59.

Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt

Harvard

Bendixen, AR, Bojesen, BB, Hüttel, H & Lybech, S 2022, 'A Generic Type System for Higher-Order Ψ-calculi', Electronic Proceedings in Theoretical Computer Science, EPTCS, bind 368, s. 43-59. https://doi.org/10.4204/EPTCS.368.3

APA

Bendixen, A. R., Bojesen, B. B., Hüttel, H., & Lybech, S. (2022). A Generic Type System for Higher-Order Ψ-calculi. Electronic Proceedings in Theoretical Computer Science, EPTCS, 368, 43-59. https://doi.org/10.4204/EPTCS.368.3

Vancouver

Bendixen AR, Bojesen BB, Hüttel H, Lybech S. A Generic Type System for Higher-Order Ψ-calculi. Electronic Proceedings in Theoretical Computer Science, EPTCS. 2022;368:43-59. https://doi.org/10.4204/EPTCS.368.3

Author

Bendixen, Alex Rønning ; Bojesen, Bjarke Bredow ; Hüttel, Hans ; Lybech, Stian. / A Generic Type System for Higher-Order Ψ-calculi. I: Electronic Proceedings in Theoretical Computer Science, EPTCS. 2022 ; Bind 368. s. 43-59.

Bibtex

@inproceedings{e99d83164a354c82a96df12b08b07533,
title = "A Generic Type System for Higher-Order Ψ-calculi",
abstract = "The Higher-Order Ψ-calculus framework (HOΨ) is a generalisation of many first- and higher-order extensions of the π-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HOπ and CHOCS can be expressed as HOΨ-calculi. In this paper we present a generic type system for HOΨ-calculi which extends previous work by H{\"u}ttel on a generic type system for first-order Ψ-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HOπ, including the type system for termination due to Demangeon et al.. Moreover, we derive a type system for the ρ-calculus, a reflective higher-order calculus proposed by Meredith and Radestock. This establishes that our generic type system is richer than its predecessor, as the ρ-calculus cannot be encoded in the π-calculus in a way that satisfies standard criteria of encodability.",
author = "Bendixen, {Alex R{\o}nning} and Bojesen, {Bjarke Bredow} and Hans H{\"u}ttel and Stian Lybech",
note = "Publisher Copyright: {\textcopyright} Bendixen, Bojesen, H{\"u}ttel and Lybech.; Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, EXPRESS/SOS 2022 ; Conference date: 12-09-2022",
year = "2022",
doi = "10.4204/EPTCS.368.3",
language = "English",
volume = "368",
pages = "43--59",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

RIS

TY - GEN

T1 - A Generic Type System for Higher-Order Ψ-calculi

AU - Bendixen, Alex Rønning

AU - Bojesen, Bjarke Bredow

AU - Hüttel, Hans

AU - Lybech, Stian

N1 - Publisher Copyright: © Bendixen, Bojesen, Hüttel and Lybech.

PY - 2022

Y1 - 2022

N2 - The Higher-Order Ψ-calculus framework (HOΨ) is a generalisation of many first- and higher-order extensions of the π-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HOπ and CHOCS can be expressed as HOΨ-calculi. In this paper we present a generic type system for HOΨ-calculi which extends previous work by Hüttel on a generic type system for first-order Ψ-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HOπ, including the type system for termination due to Demangeon et al.. Moreover, we derive a type system for the ρ-calculus, a reflective higher-order calculus proposed by Meredith and Radestock. This establishes that our generic type system is richer than its predecessor, as the ρ-calculus cannot be encoded in the π-calculus in a way that satisfies standard criteria of encodability.

AB - The Higher-Order Ψ-calculus framework (HOΨ) is a generalisation of many first- and higher-order extensions of the π-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HOπ and CHOCS can be expressed as HOΨ-calculi. In this paper we present a generic type system for HOΨ-calculi which extends previous work by Hüttel on a generic type system for first-order Ψ-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HOπ, including the type system for termination due to Demangeon et al.. Moreover, we derive a type system for the ρ-calculus, a reflective higher-order calculus proposed by Meredith and Radestock. This establishes that our generic type system is richer than its predecessor, as the ρ-calculus cannot be encoded in the π-calculus in a way that satisfies standard criteria of encodability.

UR - http://www.scopus.com/inward/record.url?scp=85137795706&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.368.3

DO - 10.4204/EPTCS.368.3

M3 - Conference article

AN - SCOPUS:85137795706

VL - 368

SP - 43

EP - 59

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

T2 - Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, EXPRESS/SOS 2022

Y2 - 12 September 2022

ER -

ID: 322570919