Zobrazeno 1 - 10
of 166
pro vyhledávání: '"VASCONCELOS, VASCO T."'
Autor:
Poças, Diogo, Vasconcelos, Vasco T.
We provide an algorithm for deciding simple grammar bisimilarity whose complexity is polynomial in the valuation of the grammar (maximum seminorm among production rules). Since the valuation is at most exponential in the size of the grammar, this giv
Externí odkaz:
http://arxiv.org/abs/2407.04063
Publikováno v:
EPTCS 401, 2024, pp. 1-10
We explore the integration of metaprogramming in a call-by-value linear lambda-calculus and sketch its extension to a session type system. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing
Externí odkaz:
http://arxiv.org/abs/2404.05475
Autor:
Fowler, Simon, Haller, Philipp, Kuhn, Roland, Lindley, Sam, Scalas, Alceste, Vasconcelos, Vasco T.
Publikováno v:
EPTCS 401, 2024, pp. 37-48
Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software
Externí odkaz:
http://arxiv.org/abs/2404.05479
Publikováno v:
Leibniz International Proceedings in Informatics (LIPIcs), 34th International Conference on Concurrency Theory (CONCUR 2023), pp.11:1-11:19
Context-free session types describe structured patterns of communication on heterogeneously-typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes
Externí odkaz:
http://arxiv.org/abs/2307.05661
Publikováno v:
EPTCS 378, 2023, pp. 1-13
We present a kind inference algorithm for the FREEST programming language. The input to the algorithm is FREEST source code with (possibly part of) kind annotations replaced by kind variables. The algorithm infers concrete kinds for all kind variable
Externí odkaz:
http://arxiv.org/abs/2304.06396
We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most con
Externí odkaz:
http://arxiv.org/abs/2304.03764
We study increasingly expressive type systems, from $F^\mu$ -- an extension of the polymorphic lambda calculus with equirecursive types -- to $F^{\mu;}_\omega$ -- the higher-order polymorphic lambda calculus with equirecursive types and context-free
Externí odkaz:
http://arxiv.org/abs/2301.08659
Publikováno v:
EPTCS 356, 2022, pp. 24-35
We present an extension of System F with higher-order context-free session types. The mixture of functional types with session types has proven to be a challenge for type equivalence formalization: whereas functional type equivalence is often rule-ba
Externí odkaz:
http://arxiv.org/abs/2203.12877
Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session ty
Externí odkaz:
http://arxiv.org/abs/2201.08275
Publikováno v:
In Theoretical Computer Science 27 June 2024 1001
