9 citations · 29 across the 12 of their papers we have counts for
15 papers
Deadlock-free Context-free Session Types
Andreia Mordido, Jorge A. Pérez
We tackle the problem of statically ensuring that message-passing programs never run into deadlocks. We focus on concurrent functional programs governed by context-free session typ…
Local Type Inference for Context-Free Session Types
Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos
We address the problem of local type inference for a language based on System F with context-free session types. We present an algorithm that leverages the bidirectional type check…
Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoung, Andreia Mordido, Frank Pfenning +1
We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this settin…
Subtyping Context-Free Session Types
Gil Silva, Andreia Mordido, Vasco T. Vasconcelos
Context-free session types describe structured patterns of communication on heterogeneously-typed channels, allowing the specification of protocols unconstrained by tail recursion.…
Kind Inference for the FreeST Programming Language
Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos
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 kin…
Parameterized Algebraic Protocols
Andreia Mordido, Janek Spaderna, Peter Thiemann +1
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. Par…
System with Context-free Session Types
Diana Costa, Andreia Mordido, Diogo Poças +1
We study increasingly expressive type systems, from -- an extension of the polymorphic lambda calculus with equirecursive types -- to -- the higher-order polymorph…
Higher-order Context-free Session Types in System F
Diana Costa, Andreia Mordido, Diogo Poças +1
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 equivalen…
Polarized Subtyping
Zeeshan Lakhani, Ankush Das, Henry DeYoung +2
Polarization of types in call-by-push-value naturally leads to the separation of inductively defined observable values (classified by positive types), and coinductively defined com…
Protocol-based Smart Contract Generation
Afonso Falcão, Andreia Mordido, Vasco T. Vasconcelos
The popularity of smart contracts is on the rise, yet breaches in reliability and security linger. Among the many facets of smart contract reliability, we concentrate on faults roo…
Polymorphic Lambda Calculus with Context-Free Session Types
Bernardo Almeida, Andreia Mordido, Peter Thiemann +1
Context-free session types provide a typing discipline for recursive structured communication protocols on bidirectional channels. They overcome the restriction of regular session…
Subtyping on Nested Polymorphic Session Types
Ankush Das, Henry DeYoung, Andreia Mordido +1
The importance of subtyping to enable a wider range of well-typed programs is undeniable. However, the interaction between subtyping, recursion, and polymorphism is not completely…
Nested Session Types
Ankush Das, Henry DeYoung, Andreia Mordido +1
Session types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is…
Mixed Sessions: the Other Side of the Tape
Filipe Casal, Andreia Mordido, Vasco T. Vasconcelos
The original paper on Mixed Sessions introduce the side A of the tape: there is an encoding of classical sessions into mixed sessions. Here we present side B: there is a translatio…
FreeST: Context-free Session Types in a Functional Language
Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos
FreeST is an experimental concurrent programming language. Based on a core linear functional programming language, it features primitives to fork new threads, and for channel creat…