Abstract
This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E , for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [19], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [19], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E , which can be seen as a refinement of system U , produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [19], which turn out to be an essential quantitative tool because they remove the confusion between âbeing a pairâ? and âbeing duplicableâ?. Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors. © LIPIcs 2020.

Abstract
We define EVL, a minimal higher-order functional language for dealing with generic events. The notion of generic event extends the well-known notion of event traditionally used in a variety of areas, such as database management, concurrency, reactive systems and cybersecurity. Generic events were introduced in the context of a metamodel to deal with obligations in access control systems. Event specifications are represented as records and we use polymorphic record types to type events in our language. We show how the higher-order capabilities of EVL can be used in the context of Complex Event Processing (CEP), to define higher-order parameterised functions that deal with the usual CEP techniques.

Abstract

Abstract
In this work, we develop a polymorphic record calculus with extensible records. Extensible records are records that can have new fields added to them, or preexisting fields removed from them. We also develop a static type system for this calculus and a sound and complete type inference algorithm. Most ML-style polymorphic record calculi that support extensible records are based on row variables. We present an alternative construction based on the polymorphic record calculus developed by Ohori. Ohori based his polymorphic record calculus on the idea of kind restrictions. This allowed him to express polymorphic operations on records such as field selection and modification. With the addition of extensible types, we were able to extend Ohori’s original calculus with other powerful operations on records such as field addition and removal. © S. Alves & M. Ramos

Abstract

Abstract
Weak linearisation was defined years ago through a static characterization of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general ? -terms and weak-linear ? -terms, whilst preserving normal forms by reduction. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.