Fundamenta Informaticae - Volume 170, issue 1-3

Authors: Altenkirch, Thorsten | Schubert, Aleksy

Article Type: Other

DOI: 10.3233/FI-2019-1852

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. v-vi, 2019

Authors: Bezem, Marc | Coquand, Thierry

Article Type: Research Article

Abstract: We give a constructive proof of Skolem’s Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.

Keywords: Skolem’s theorem, coherent logic, proof theory

DOI: 10.3233/FI-2019-1853

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

Authors: Bono, Viviana

Article Type: Research Article

Abstract: We discuss Magda ten years after its design. Magda is a mixin-oriented programming language and its goal is to improve code modularity and, as a consequence, code reuse. The aim of this paper is to survey Magda and position it in today’s programming language scenarios.

Keywords: Object-oriented programming language, mixin, modularity, code reuse

DOI: 10.3233/FI-2019-1854

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 15-38, 2019

Authors: Downen, Paul | Ariola, Zena M. | Ghilezan, Silvia

Article Type: Research Article

Abstract: For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are …not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe. Show more

Keywords: Intersection types, union types, duality, sequent calculus, discipline, type safety, strong normalization, soundness and completeness, reducibility candidates, symmetric candidates

DOI: 10.3233/FI-2019-1855

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 39-92, 2019

Authors: Dudenhefner, Andrej | Rehof, Jakob

Article Type: Research Article

Abstract: We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we simplify the existing proof, reducing simple semi-Thue systems to intersection type inhabitation in the original Coppo-Dezani type assignment system. Additionally, we outline a direct reduction from the Turing machine halting problem to intersection type inhabitation. Second, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of “type theory inside type theory”.

DOI: 10.3233/FI-2019-1856

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 93-110, 2019

Authors: Santo, José Espírito | Matthes, Ralph | Pinto, Luís

Article Type: Research Article

Abstract: If we consider as “member” of a simple type the outcome of any successful (possibly infinite) run of bottom-up proof search that starts from the type, then several concepts of “finiteness” for simple types are possible: the finiteness of the search space, the finiteness of any member, or the finiteness of the number of finite members (in other words, the inhabitants). In this paper we show that these three concepts are instances of the same parameterized notion of finiteness, and that a single, parameterized proof shows the decidability of all of them. One instance of this result means that termination …of proof search is decidable. A separate result is that emptiness is also decidable (where emptiness is absence of “members” as above, not just absence of inhabitants). This fact is an ingredient of the main decidability result, but it also has a different application, the definition of the pruned search space - the one where branches leading to failure are chopped off. We conclude with our version of König’s lemma for simple types: a simple type has an infinite member exactly when the pruned search space is infinite. Show more

Keywords: lambda-calculus, proof search, coinduction, decision procedure

DOI: 10.3233/FI-2019-1857

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 111-138, 2019

Authors: Geuvers, Herman | van der Giessen, Iris | Hurkens, Tonny

Article Type: Research Article

Abstract: We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction . In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table. This yields natural deduction rules for each connective separately. Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions. The aim is to remove all convertibilities and obtain a deduction in normal form. In general, conversion of truth table …natural deductions is non-deterministic, which makes it more challenging to study. It has already been shown that this conversion is weakly normalizing. To prove strong normalization, we construct a conversionpreserving translation from deductions to terms in an extension of simply typed lambda calculus which we call parallel simply typed lambda calculus and which we prove to be strongly normalizing. This makes it possible to get a grip on the non-deterministic character of conversion in the intuitionistic truth table natural deduction system. Show more

Keywords: Natural deduction, truth tables, intuitionistic logic, detour conversion, permutation conversion, strong normalization

DOI: 10.3233/FI-2019-1858

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 139-176, 2019

Authors: Hupel, Lars

Article Type: Research Article

Abstract: Type classes are a well-known extension to various type systems. Classes usually participate in type inference; that is, the type checker will automatically deduce class constraints and select appropriate instances. Compilers for such languages face the challenge that concrete instances are generally not directly mentioned in the source text. In the runtime, type class operations need to be packaged into dictionaries that are passed around as pointers. This article presents the most common approach for compilation of type classes – the dictionary construction – carried out in a trustworthy fashion in Isabelle/HOL, a proof assistant. The result is an automatic …routine that eliminates occurences of classes and instances from a set of definitions and proves a theorem relating old and new definitions. Show more

Keywords: Isabelle, HOL, type systems, type classes, interactive theorem proving, dictionary construction

DOI: 10.3233/FI-2019-1859

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 177-205, 2019

Authors: Kfoury, Assaf

Article Type: Research Article

Abstract: This article traces in broad strokes the evolution of the intimate relationship between mathematical logic and computer science. The emphasis is on turning points in this relationship, i.e ., moments when new directions of research were opened and new connections were established between the two fields. The article is not a comprehensive account and history of the relationship, but a personal perspective of a profoundly changed, and still changing, inter-dependence between two mainstays of the mathematical disciplines.

DOI: 10.3233/FI-2019-1860

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 207-221, 2019

Authors: Kurata, Toshihiko | Fujita, Ken-etsu

Article Type: Research Article

Abstract: We study a version of the Stone duality between the Alexandrov spaces and the completely distributive algebraic lattices. This enables us to present lattice-theoretical models of second-order intuitionistic propositional logic which correlates with the Kripke models introduced by Sobolev. This can be regarded as a second-order extension of the well-known correspondence between Heyting algebras and Kripke models in the semantics of intuitionistic propositional logic.

Keywords: second-order intuitionistic propositional logic, complete Heyting algebra, completeness theorem

DOI: 10.3233/FI-2019-1861

Citation: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 223-240, 2019

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