Search

We show characterisation results for normalisation, head-normalisation, and strong normalisation for λ μ using intersection types. We reach these results for a strict notion of type assignment for λ μ that is the natural restriction of the domain-based system of van Bakel et al. (2011) for λ μ by limiting the type inclusion relation to just intersection elimination. We show that this system respects β μ-equality, by showing both soundness and completeness results. We then define a notion of reduction on derivations that corresponds to cut-elimination, and show that this is strongly normalisable. We use this strong normalisation result to show an approximation result, and through that a characterisation of head-normalisation. Using the approximation result, we show that there is a very strong relation between the system of van Bakel et al. (2011) and ours. We then introduce a notion of type assignment that eliminates ω as an assignable type, and show, using the strong normalisation result for derivation reduction, that all terms typeable in this system are strongly normalisable as well, and show that all strongly normalisable terms are typeable. We conclude by adding type variables to our system, and show that system essentially is that of van Bakel (2010b).

We study the strict type assignment for lambda-mu that is presented in [van Bakel'16]. We define a notion of approximants of lambda-mu-terms, show that it generates a semantics, and that for each typeable term there is an approximant that has the same type. We show that this leads to a characterisation via assignable types for all terms that have a head normal form, and to one for all terms that have a normal form, as well as to one for all terms that are strongly normalisable., Comment: In Proceedings ITRS 2016, arXiv:1702.01874

We study the lambda-mu-calculus, extended with explicit substitution, and define a compositional output-based interpretation into a variant of the pi-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for lambda-mu -- one based on weak reduction, two modelling weak head-reduction and weak explicit head reduction (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation -- and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes., Comment: In Proceedings CL&C 2014, arXiv:1409.2593

We investigate the notion of orchestrated compliance for client/server interactions in the context of session contracts. Devising the notion of orchestrator in such a context makes it possible to have orchestrators with unbounded buffering capabilities and at the same time to guarantee any message from the client to be eventually delivered by the orchestrator to the server, while preventing the server from sending messages which are kept indefinitely inside the orchestrator. The compliance relation is shown to be decidable by means of 1) a procedure synthesising the orchestrators, if any, making a client compliant with a server, and 2) a procedure for deciding whether an orchestrator behaves in a proper way as mentioned before., Comment: In Proceedings ICE 2015, arXiv:1508.04595

With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus X, a substitution-free language that enjoys the Curry-Howard correspondence with respect to the implicative fragment of Gentzen's sequent calculus for classical logic. We investigate the minimal requirements for such a system to be complete i.e. closed under redex expansion, and show that the non-logical nature of both intersection and union types disturbs the soundness i.e. closed uder reduction properties. This implies that this notion of intersection-union type assignment needs to be restricted to satisfy soundness as well, making it unsuitable to define a semantics. We will look at two confluent notions of reduction, called Call-by-Name and Call-by-Value, and prove soundness results for those.

This article will show the usefulness and elegance of strict intersection types for the Lambda Calculus, that are strict in the sense that they are the representatives of equivalence classes of types in the BCD-system [Barendregt et al. 1983]. We will focus on the essential intersection type assignment; this system is almost syntax directed, and we will show that all major properties hold that are known to hold for other intersection systems, like the approximation theorem, the characterization of (head/strong) normalization, completeness of type assignment using filter semantics, strong normalization for cut-elimination and the principal pair property. In part, the proofs for these properties are new; we will briefly compare the essential system with other existing systems.

$\X$is an untyped continuation-style formal language with a typed subset that provides a Curry–Howard isomorphism for a sequent calculus for implicative classical logic.$\X$can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make${\X}$an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for$\X$; in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the λ-calculus, Bloo and Rose's calculus of explicit substitutions λx, Parigot's λμ and Curien and Herbelin's$\lmmt$.${\X}$was first presented in Lengrand (2003), where it was called the λξ-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).

This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types for a system with ‘w and a ≤-relation that is contra-variant over arrow types. The technique applied is to define reduction on derivations and to show a strong normalisation result for this reduction. From this result, the characterisation of strong normalisation and the approximation result will follow easily; the latter, in its turn, will lead to the characterisation of (head) normalisability.

Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order ς-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence.