-
Notifications
You must be signed in to change notification settings - Fork 0
Home
The document contains selected topics on Type Theory. The main source of information is Pierce's Types and Programming Languages. In this wiki we outline the topics covered so far, suggest new topics to cover as well as modifications that the document shall undergo.
-
The Type-Free Lambda Calculus. The goal of this section is to present the syntax and semantics of the lambda calculus and explain basic concepts that will be used throughout the document as variable substitution, operation semantics, ... Status: Incomplete.
-
Syntax and Semantics of STLC. This sections adds types to the previous presented type-free lambda calculus. Status: Complete, needs revision. Perhaps should be merged with the next section.
-
Typing in STLC. The main goal of this section is to prove safety of the previous type systems. Status: Complete.
4.Introducting Naturals and Booleans. This sections adds new syntactic categories to the language: the bools and the naturals. Status: Incomplete.
5.Normalizaiton of STLC. The goal of this section is to prove the normalisation of the STLC. It discusses the technique of the logical relations. Status: Incomplete.
6._Syntax and Semantics of STLC + References. Adds references to the previous language. Status: Complete.
7.Typing in STLC + References. Adds a type system to the previous language. Proves type safety. Status: Complete.
8.Polymorphism. Discusses polymorphism. Introduces system F. Status: Incomplete.
Obs: The notation used throughout the document has to be revised.