A Generic Type System for Higher-Order Ψ-calculi
Research output: Contribution to journal › Conference article › Research › peer-review
Standard
A Generic Type System for Higher-Order Ψ-calculi. / Bendixen, Alex Rønning; Bojesen, Bjarke Bredow; Hüttel, Hans; Lybech, Stian.
In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 368, 2022, p. 43-59.Research output: Contribution to journal › Conference article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
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