Fundamenta Informaticae - Volume 170, issue 1-3

Authors: Manzonetto, Giulio | Pagani, Michele | Ronchi Della Rocca, Simona

Article Type: Research Article

Abstract: Despite the fact that call-by-value λ -calculus was defined by Plotkin in 1977, we believe that its theory of program approximation is still at the beginning. A problem that is often encountered when studying its operational semantics is that, during the reduction of a λ -term, some redexes remain stuck (waiting for a value). Recently, Carraro and Guerrieri proposed to endow this calculus with permutation rules, naturally arising in the context of linear logic proof-nets, that succeed in unblocking a certain number of such redexes. In the present paper we introduce a new class of models of call-by-value λ -calculus, …arising from non-idempotent intersection type systems. Beside satisfying the usual properties as soundness and adequacy, these models validate the permutation rules mentioned above as well as some reductions obtained by contracting suitable λI -redexes. Thanks to these (perhaps unexpected) features, we are able to demonstrate that every model living in this class satisfies an Approximation Theorem with respect to a refined notion of syntactic approximant. While this kind of results often require impredicative techniques like reducibility candidates, the quantitative information carried by type derivations in our system allows us to provide a combinatorial proof. Show more

Keywords: lambda calculus, call-by-value, relational semantics, approximation theorem, intersection types

DOI: 10.3233/FI-2019-1862

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 241-265, 2019

Authors: Severi, Paula | Dezani-Ciancaglini, Mariangiola

Article Type: Research Article

Abstract: Multiparty sessions are concurrent processes, which allow several participants to communicate by sending and receiving messages. We consider an observational preorder of processes, that captures the idea that the whole session remains correct after replacing one process by another one. This preorder is characterised by means of a structural preorder between processes, which mimics the subtyping relation between session types from the literature.

DOI: 10.3233/FI-2019-1863

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 267-305, 2019

Authors: Statman, Rick

Article Type: Research Article

Abstract: Solving the Entscheidungsproblem was a challenge first posed by David Hilbert in 1928, and solutions to decision problems are perhaps the most prized posessions in logic. Pawel Urzyczyn has a number of these, one of which I will discuss below. However, let me remind you of Michael Rabin describing his time with Dana Scott at IBM prior to their Turing award winning paper Finite automata and their decision problems “So we both went, in 1957 to IBM and the location was the so-called Lamb Estate [Robert S. Lamb estate], a wonderful place, while the Princeton Laboratory, designed by Sarason, …the Watson Laboratory was in stages of construction. The Lamb Estate, very appropriately, used to be, before that, an Insane Asylum. All those buildings were building where kooks were housed...” [1]. This is what IBM thought of decision problems. In this note we give a new proof of the undecidability of the inhabitation problem for intersection types. Show more

DOI: 10.3233/FI-2019-1864

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 307-324, 2019