Wyniki wyszukiwania - BazTech

1

The Duality of Classical Intersection and Union Types

Downen Paul, Ariola Zena M., Ghilezan Silvia

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

39--92

EN

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.

2

Towards a Logic for Union Types

Stavrinos Y., Veneti A.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

275-302

EN

We examine a logical foundation for the intersection and union types assignment system (IUT). The proposed system is Intersection and Union Logic (IUL), an extension of Intersection Logic (IL) with the canonical rules for union. We investigate two different formalisms for IUL, as well as its properties and its relation with minimal intuitionistic logic.

3

Strong Normalization in the π-calculus with Intersection and Union Types

Piccolo M.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

227-252

EN

In this work we present an extension of the linear typing discipline for π-calculus, introduced by Yoshida,Honda and Berger, with Intersection and Union Types. We show that we are able to define a typing system for the π-calculus, which guarantees that every well-typed term is strongly normalizing. This typing system is an extension of that presented in [30] since it is able to type more terms than that presented there.

4

Completeness and Soundness Results for χ with Intersection and Union Types

Bakel S. van

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

1-41

EN

With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus χ, 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.

5

Processing semi-structured data in object bases

Subieta K., Leszczyłowski J., Ulidowski I.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

1998

|

nr 852

3-51

EN

We adress the problem of null values and other forms of semi-structured data in object-oriented databases. Various aspects and issues concerning semi-structured data that are currently presented in the litarature are discussed in the paper. We propose a new universal approach to semi-structured data based on the idea of absent objects. The idea covers null values and union types and can be smoothly combined with the idea of default values. We introduce a simple model of object store that is similar to the Tsimmis model. In contrast to the main stream of the research, our basic assumption is that semi-structured data are not only to be queried but also processed by an integrated query/programming language. To this end we discuss query language constructs that are relevant to query semi-structured data and corresponding issues in programming languages. The idea follows the stack-based approach to integrated query/programming languages that we have implemented in the LOQIS system. Finally we briefly discuss a new approach to polymorphic typing of semi-structured data that is implemented in LOQIS.

PL

W pracy rozpatrywany jest problem wartości zerowych i innych rodzajów nie w pełni ustrukturalizowanych danych w obiektowych bazach danych. Omawiane są różne aspekty i zagadnienia dotyczące takich danych, które występują w literaturze przedmiotu. Proponowane jest nowe, uniwersalne podejście do nie w pełni ustrukturalizowanych danych oparte na koncepcji nieobecnych obiektów. Podejście to obejmuje wartości zerowe i typy unii a także może być spójnie połączone z koncepcją wartości domyslnych. Przedstawiamy prosty model składu obiektów podobny do składu używanego w modelu projektu Tsimmis. W przeciwieństwie do głównego nurtu badań w tej dziedzinie, zakładamy, że nie w pełni ustrukturalizowane dane nie tylko powinny być dostępne przez pytania języka zapytań, ale także powinny być przetwarzane przez zintegrowane języki zapytań i programowania. Omawiamy odpowiednie konstrukcje związane z odpytywaniem takich danych i odpowiadające im zagadnienia w językach programowania. Koncepcje przedstawione są w ramach podejścia stosowego do integracji języków zapytań i programowania, które jest zaimplementowane w systemie LOQIS. Na koniec krótko omawiamy nowe podejście do polimorficznego typowania nie w pełni ustrukturalizowanych danych, które także jest zaimplementowane w LOQIS-e.