L.Yu. Ismailova1, S.V. Kosikov2

1 National Research Nuclear University MEPhI (Moscow, Russia)

2 LLC "JurInfoR" (Moscow, Russia)

1 LYIsmailova@mephi.ru, 2 kosikov.s.v@gmail.com

Currently there are two main methods for constructing type systems for lambda calculus: following the Church approach and following the Curry approach. In systems based on the Church approach, terms represent annotated versions of untyped terms. Each term has a type, which is usually unique (up to an equivalence relation) and is derived from the term annotation. In the typed lambda calculus à la Curry, each term has a set of possible types. This set can be empty, singleton, or consist of several (possibly infinitely many) elements. Aim of article to present a method for constructing type systems with different approaches, highlight their advantages and disadvantages, and to determine the possibility of their application for constructing a domain-oriented type system when constructing practical applicative systems.

A method for constructing type systems based on different approaches is presented, and recommendations for their application in constructing a domain-oriented type system are given. The results of the work can be used in the selection or construction of an tooling system to support practical applicative systems.

Ismailova L.Yu., Kosikov S.V. Domain-specific type systems in the church and curry formalism. Information-measuring and Control Systems. 2024. V. 22. № 5. P. 39−45. DOI: https://doi.org/10.18127/j20700814-202405-05 (in Russian)

1. Volfengagen V.E. Metody i sredstva vychislenii s ob'ektami. Applikativnye vychislitelnye sistemy. M.: YurInfoR. 2004. 787 s. ISBN 5-89158-100-0. (in Russian)
2. Wolfengagen V., Ismailova L., Kosikov S. When and Where Conceptual Maths Equals to Conceptual Modeling: Reasons for Using in Cognitive Modeling. Proceedings of BICA*AI. 2023.
3. Ismailova L., Wolfengagen V., Kosikov S. Elements of semantic analysis based on lambda-calculus. Proceedings of BICA*AI. 2022.
4. Slieptsov I., Ismailova L., Kosikov S. Analysis and comparison of generators of words of context-sensitive language on example of typed λ-calculus. Proceedings of BICA*AI. 2022.
5. Williams C., Stay M. Native Type Theory. 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
6. Altenkirch T., Kaposi A. A container model of type theory. 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
7. Mc Bride C., Forsberg F.N. Functorial Adapters. 27th International Conference on Types for Proofs and Programs. 2021. https://types21.liacs.nl/.
8. Dybjer P., Setzer A. Implementing Martin-Löf’s Meaning Explanations for Intuitionistic Type Theory in Agda. 28th International Conference on Types for Proofs and Programs. 2022. https://types22.inria.fr/.
9. Booij A. Exhaustive testing of property testers. 28th International Conference on Types for Proofs and Programs. 2022. https://types22.inria.fr/.
10. Shulman M. The unifying power of modal type theory. The Second International Conference on Homotopy Type Theory (HoTT). 2023. https://hott.github.io/HoTT-2023//.