4 citations · 11 across the 11 of their papers we have counts for
12 papers
Linearising Explicit Substitutions using Intersection Types
Ana Jorge Almeida, Sandra Alves, Mário Florido
Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion inclu…
CoMPSeT: A Framework for Comparing Multiparty Session Types
Telmo Ribeiro, José Proença, Mário Florido
Concurrent systems are often complex and difficult to design. Choreographic languages, such as Multiparty Session Types (MPST), allow the description of global protocols of interac…
Linear Rank Intersection Types
Fábio Reis, Sandra Alves, Mário Florido
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems…
Execution Time Program Verification With Tight Bounds
Ana Carolina Silva, Manuel Barbosa, Mario Florido
This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: ap…
Typed SLD-Resolution: Dynamic Typing for Logic Programming
João Barbosa, Mário Florido, Vítor Santos Costa
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that comp…
Structural Rules and Algebraic Properties of Intersection Types
Sandra Alves, Mário Florido
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection ty…
Data Type Inference for Logic Programming
João Barbosa, Mário Florido, Vítor Santos Costa
In this paper we present a new static data type inference algorithm for logic programming. Without the need of declaring types for predicates, our algorithm is able to automaticall…
A Three-Valued Semantics for Typed Logic Programming
João Barbosa, Mário Florido, Vítor Santos Costa
Types in logic programming have focused on conservative approximations of program semantics by regular types, on one hand, and on type systems based on a prescriptive semantics def…
Non-Blocking Concurrent Imperative Programming with Session Types
Miguel Silva, Mário Florido, Frank Pfenning
Concurrent C0 is an imperative programming language in the C family with session-typed message-passing concurrency. The previously proposed semantics implements asynchronous (non-b…
Liquid Intersection Types
Mário Pereira, Sandra Alves, Mário Florido
We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise ty…
Proceedings First International Workshop on Linearity
Mário Florido, Ian Mackie
This volume contains the proceedings of LINEARITY 2009: the first International Workshop on Linearity, which took place 12th September 2009 in Coimbra, Portugal. The workshop was a…
Linear Recursion
Sandra Alves, Maribel Fernández, Mário Florido +1
We define two extensions of the typed linear lambda-calculus that yield minimal Turing-complete systems. The extensions are based on unbounded recursion in one case, and bounded re…