WebPie: A Tiny Slice of Dependent Typing
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916197704925184 |
|---|---|
| author | Scholliers, Christophe |
| author_facet | Scholliers, Christophe |
| contents | Dependently typed programming languages have become increasingly relevant in recent years. They have been adopted in industrial strength programming languages and have been extremely successful as the basis for theorem provers. There are however, very few entry level introductions to the theory of language constructs for dependently typed languages, and even less sources on didactical implementations. In this paper, we present a small dependently typed programming language called WebPie. The main features of the language are inductive types, recursion and case matching. While none of these features are new, we believe this article can provide a step forward towards the understanding and systematic construction of dependently typed languages for researchers new to dependent types. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_05457 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | WebPie: A Tiny Slice of Dependent Typing Scholliers, Christophe Programming Languages Logic in Computer Science Symbolic Computation Dependently typed programming languages have become increasingly relevant in recent years. They have been adopted in industrial strength programming languages and have been extremely successful as the basis for theorem provers. There are however, very few entry level introductions to the theory of language constructs for dependently typed languages, and even less sources on didactical implementations. In this paper, we present a small dependently typed programming language called WebPie. The main features of the language are inductive types, recursion and case matching. While none of these features are new, we believe this article can provide a step forward towards the understanding and systematic construction of dependently typed languages for researchers new to dependent types. |
| title | WebPie: A Tiny Slice of Dependent Typing |
| topic | Programming Languages Logic in Computer Science Symbolic Computation |
| url | https://arxiv.org/abs/2404.05457 |