We present FJ&λ⋆, a new core calculus that extends Featherweight Java (FJ) with interfaces, λ-expressions, intersection types and a form of dynamic type. Intersection types can be used anywhere, in particular to specify target types of λ-expressions. The dynamic type is exploited to specify parts of the class tables and programs we want to exclude temporarily from static typing. Our main result is the gradual guarantee, which says that if a program is well typed in a class table, then replacing type annotations (from the program and from the class table) with the dynamic type always produces a program that is still well typed in the obtained class table. Furthermore, if a typed program evaluates to a value in a class table, then replacing type annotations with dynamic types always produces a program that evaluates to the same value in the obtained class table.

Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their strengths. We incorporate these two contributions in a single typed calculus and define an operational semantics with type cast annotations. We also prove several crucial properties of the type system, namely that types are preserved during compilation and evaluation, and that the refined criteria for gradual typing holds.

Abstract CLP(H) is an instantiation of the general constraint logic programming scheme with the constraint domain of hedges. Hedges are finite sequences of unranked terms, built over variadic function symbols and three kinds of variables: for terms, for hedges, and for function symbols. Constraints involve equations between unranked terms and atoms for regular hedge language membership. We study algebraic semantics of CLP(H) programs, define a sound, terminating, and incomplete constraint solver, investigate two fragments of constraints for which the solver returns a complete set of solutions, and describe classes of programs that generate such constraints.

This article presents a semantics-based program verification framework for critical embedded real-time systems using the worst-case execution time (WCET) as the safety parameter. The verification algorithm is designed to run on devices with limited computational resources where efficient resource usage is a requirement. For this purpose, the framework of abstract-carrying code (ACC) is extended with an additional verification mechanism for linear programming (LP) by applying the certifying properties of duality theory to check the optimality of WCET estimates. Further, the WCET verification approach preserves feasibility and scalability when applied to multicore architectural models. The certifying WCET algorithm is targeted to architectural models based on the ARM instruction set and is presented as a particular instantiation of a compositional data-flow framework supported on the theoretic foundations of denotational semantics and abstract interpretation. The data-flow framework has algebraic properties that provide algorithmic transformations to increase verification efficiency, mainly in terms of verification time. The WCET analysis/verification on multicore architectures applies the formalism of latency-rate (LR) servers, and proves its correctness in the context of abstract interpretation, in order to ease WCET estimation of programs sharing resources.

In this article we discuss three different notions of linearity: syntactical, operational and denotational. We briefly define each notion of linearity, pointing out some of the main results in the area, and describe applications of linear languages and type systems.

Journal Article Linearity in Computation Get access Mário Florido, Mário Florido Search for other works by this author on: Oxford Academic Google Scholar Ian Mackie Ian Mackie Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 24, Issue 3, June 2014, Pages 511–512, https://doi.org/10.1093/logcom/exs024 Published: 12 June 2012

This paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this paper, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of lazy potential. We present our analysis as a proof system for predicting heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury's natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis.

We show that the full PCF language can be encoded in L_rec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for L_rec, exploiting its linearity.

The linear lambda calculus, where variables are restricted to occur in terms exactly once, has a very weak expressive power: in particular, all functions terminate in linear time. In this paper we consider a simple extension with natural numbers and a restricted iterator: only closed linear functions can be iterated. We show properties of this linear version of Godel's T using a closed reduction strategy, and study the class of functions that can be represented. Surprisingly, this linear calculus offers a huge increase in expressive power over previous linear versions of T, which are 'closed at construction' rather than 'closed at reduction'. We show that a linear T with closed reduction is as powerful as T.

Maintaining large Web sites and verifying their semantic content is a difficult task. In this paper we propose a framework for syntactic validation, semantic verification and automatic correction of Web sites based on the logic programming language XCentric. Here we purpose a new approach conciliating the highly declarative model of XCentric with compile and run time verification techniques, mainly based on type checking to automatically repair and audit Web sites. The result is an easy to follow model to improve and audit Web site content.

In this paper we present a notion of expansion of a term in the lambda-calculus which transforms terms into linear terms. This transformation replaces each occurrence of a variable in the original term by a fresh variable taking into account non-trivial implications in the structure of the term caused by these simple replacements. We prove that the class of terms which can be expanded is the same of terms typable in an Intersection Type System, i.e. the strongly normalizable terms. We then show that expansion is preserved by weak-head reduction, the reduction considered by functional programming languages.