Geodesic
A recursive inclusion checker for recursively defined subtypes
Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 414-433.

Voir la notice de l'article provenant de la source Math-Net.Ru

We present a tableaux procedure that checks logical relations between recursively defined subtypes of recursively defined types and apply this procedure to the problem of resolving ambiguous names in a programming language. This work is part of a project to design a new programming language suitable for efficient implementation of logic. Logical formulas are tree-like structures with many constructors having different arities and argument types. Algorithms that use these structures must perform case analysis on the constructors, and access subtrees whose type and existence depend on the constructor used. In many programming languages, case analysis is handled by matching, but we want to take a different approach, based on recursively defined subtypes. Instead of matching a tree against different constructors, we will classify it by using a set of disjoint subtypes. Subtypes are more general than structural forms based on constructors, we expect that they can be implemented more efficiently, and in addition can be used in static type checking. This makes it possible to use recursively defined subtypes as preconditions or postconditions of functions. We define the types and the subtypes (which we will call adjectives), define their semantics, and give a tableaux-based inclusion checker for adjectives. We show how to use this inclusion checker for resolving ambiguous field references in declarations of adjectives. The same procedure can be used for resolving ambiguous function calls.
Keywords: programming language design, type systems, theorem proving
Mots-clés : compiler construction. 
@article{MAIS_2021_28_4_a6,
     author = {H. de Nivelle},
     title = {A recursive inclusion checker for recursively defined subtypes},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {414--433},
     publisher = {mathdoc},
     volume = {28},
     number = {4},
     year = {2021},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a6/}
}
TY  - JOUR
AU  - H. de Nivelle
TI  - A recursive inclusion checker for recursively defined subtypes
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2021
SP  - 414
EP  - 433
VL  - 28
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a6/
LA  - en
ID  - MAIS_2021_28_4_a6
ER  - 
%0 Journal Article
%A H. de Nivelle
%T A recursive inclusion checker for recursively defined subtypes
%J Modelirovanie i analiz informacionnyh sistem
%D 2021
%P 414-433
%V 28
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a6/
%G en
%F MAIS_2021_28_4_a6
H. de Nivelle. A recursive inclusion checker for recursively defined subtypes. Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 414-433. http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a6/

[1] Y. Minsky, A. Madhavapeddy, J. Hickey, Real World OCaml (functional programming for the masses), O'Reilly, 2013

[2] G. Hutton, Programming in Haskell, second edition, Cambridge University Press, 2016 | Zbl

[3] M. Odersky, L. Spoon, B. Venners, Programming in Scala, Third Edition, Artima Press, 2007–2016

[4] P. Rondon, M. Kawaguchi, R. Jhala, “Liquid Types”, Programming Language Design and Implementation, PLDI, eds. R. Gupta, S. Amarasinghe, ACM, 2009, 159–169

[5] R. Jhala, N. Vazou, “Refinement Types: A Tutorial”, Foundations and Trends in Programming Languages, 6:3–4 (2021), 159–317 | DOI

[6] S. Klabnik, C. Nichols, The Rust Programming Language, No Starch Press, 2019

[7] M. Gelfond, V. Lifschitz, “The Stable Model Semantics for Logic Programming”, Fifth International Conference and Symposium on Logic Programming, eds. R. Kowalski, K. Bowen, MIT Press, 1988, 1070–1080

[8] G. Tseytin, “On the complexity of Derivation in the Propositional Calculus”, Studies in Constructive Mathematics and Mathematical Logic, Zapiski Nauchnykh Seminarov, v. II, ed. A. Slisenko, 1970, 115–125