Zobrazeno 1 - 10
of 62
pro vyhledávání: '"Florido, Mário"'
MLsub is a minimal language with a type system combining subtyping and parametric polymorphism and a type inference algorithm which infers compact principal types. Simple-sub is an alternative inference algorithm which can be implemented efficiently
Externí odkaz:
http://arxiv.org/abs/2407.06747
Here we define a new unification algorithm for terms interpreted in semantic domains denoted by a subclass of regular types here called deterministic regular types. This reflects our intention not to handle the semantic universe as a homogeneous coll
Externí odkaz:
http://arxiv.org/abs/2404.16406
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to
Externí odkaz:
http://arxiv.org/abs/2211.17186
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: approximations of the worst-case execution time, exact time reasoning, a
Externí odkaz:
http://arxiv.org/abs/2210.11105
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative semantics, whic
Externí odkaz:
http://arxiv.org/abs/2208.00192
Autor:
Alves, Sandra, Florido, Mário
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 type system. Expansion relates terms typed by associative, commutative a
Externí odkaz:
http://arxiv.org/abs/2204.12376
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 automatically assign types to predicates which, in most cases, correspond to the d
Externí odkaz:
http://arxiv.org/abs/2108.06562
Publikováno v:
EPTCS 306, 2019, pp. 36-51
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 defined for typed programs, on the other. In this paper, we define a new
Externí odkaz:
http://arxiv.org/abs/1909.08232
Publikováno v:
EPTCS 238, 2017, pp. 64-72
Concurrent C0 is an imperative programming language in the C family with session-typed message-passing concurrency. The previously proposed semantics implements asynchronous (non-blocking) output; we extend it here with non-blocking input. A key idea
Externí odkaz:
http://arxiv.org/abs/1701.04920
Publikováno v:
EPTCS 177, 2015, pp. 24-42
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 types than in the original refinement system. We have been able to prove
Externí odkaz:
http://arxiv.org/abs/1503.04908