W dniach od 2 kwietnia do 5 kwietnia 2024 r. prowadzone będą prace związane z wdrożeniem nowej wersji systemu Repozytorium UJ. Nie będzie możliwe wprowadzanie nowych informacji do repozytorium. Za utrudnienia przepraszamy.
Kwantyfikacja jest ważnym pojęciem w teorii typów, które zaimplementowane jest w wielu nowoczesnych językach programowania. Wprowadza ona dwa istotne mechanizmy: polimorfizm parametryczny oraz abstrakcję danych. Wiążę się również z dwoma kluczowymi właściwościami systemów typów: ekspresyjnością oraz rozstrzygalnością problemu sprawdzania typu. W niniejszej pracy przedstawię teoretyczne podstawy kwantyfikacji opartej na rachunku lambda, opiszę kilka podstawowych systemów typów, które zawierają kwantyfikację oraz omówię kwantyfikację w kontekście trzech nowoczesnych języków programowania: Javy, Scali oraz języka C#.
abstrakt w j. angielskim:
Quantification is an important concept in type theory and is employed in numerous modern programming languages. It introduces two vital mechanisms: parametric polymorphism and data abstraction. It is closely related to crucial theoretical properties of type systems: expressiveness and decidability of type-checking. In this paper I am going to briefly introduce theoretical foundations of quantification based on the lambda calculus, describe some basic type systems, which incorporate quantification, and finally discuss quantification in the context of three modern programming languages: Java, Scala and C#.
słowa kluczowe w j. polskim:
teoria typów, rachunek lambda, sprawdzanie typu, kwantyfikacja, języki programowania, systemy typów
słowa kluczowe w j. angielskim:
type theory, lambda calculus, type-checking, quantification, programming languages, type systems
wydział: instytut / zakład / katedra:
Wydział Matematyki i Informatyki
typ:
praca licencjacka
Pliki tej pozycji
Plik
Rozmiar
Format
Przeglądanie
Nie ma plików powiązanych z tą pozycją.
Pozycja umieszczona jest w następujących kolekcjach