Adobe PDF
(420.13 kB)
| Title Details: | |
|
Type theory |
|
| Authors: |
Stefaneas, Petros Koletsos, Georgios |
| Reviewer: |
Dimitrakopoulos, Konstantinos |
| Description: | |
| Abstract: |
An Introduction to Type Theory. A historical overview of the development of type theory and its connection to the foundations of Mathematics. Church’s simply typed lambda calculus. Typing in Church-style and Curry-style. Strong normalization and expressiveness theorems. Extension of the system – Gödel’s System T. Connection with the functional programming language ML. Polymorphism and Girard–Reynolds System F. Expressiveness and programming with polymorphic types. The strong normalization theorem and the reducibility method. Constructive logic and natural deduction systems. The Curry–Howard isomorphism between proofs in constructive logic and typed lambda calculus. The Curry–Howard correspondence, and its extension to classical logic. Programming using classical proofs. Applications of type theory in computer science.
|
| Technical Editors: |
Stavrinos, Giorgos |
| Type: |
Chapter |
| Creation Date: | 2015 |
| Item Details: | |
| License: |
http://creativecommons.org/licenses/by-nc-nd/3.0/gr |
| Handle | http://hdl.handle.net/11419/4529 |
| Bibliographic Reference: | Stefaneas, P., & Koletsos, G. (2015). Type theory [Chapter]. In Stefaneas, P., & Koletsos, G. 2015. Applications of logic in computer science [Undergraduate textbook]. Kallipos, Open Academic Editions. https://hdl.handle.net/11419/4529 |
| Language: |
Greek |
| Is Part of: |
Applications of logic in computer science |
| Publication Origin: |
Kallipos, Open Academic Editions |