Cost Semantics for Parallelism
Cost semantics is to discuss: How long do programs run (abstractly)?
Programming Language Theory
Imperative Programming - Algol
Haskell is a dialect Algol!
Recursive Types
Recap for Product/Sum Types
Recursive Programs
Partial Functions
Parametricity - Logical Equivalence for Polymorphic Types
Hereditary Termination and Logical Equivalence Recap
Polymorphic Functional Programming
An example to start off
Equational Reasoning
The main question is, how do we define two programs are equal, and how do we prove it.
Basic Computational Type Theory
Family of Types
Type Theory Foundations
We can think of Type Theory as being a catalog of a variety of notions of computation. The type structure determines the “programming language features”. For...
Sequent Calculus
Verifications
Computational Interpretations
Here we will talk about computational interpretations by the example of lax logic. Hope from the example we can have sense of how logic and PL are connected.
Judgements and Propositions
We state “A is true”, then “A” is a proposition, and “A is true” as a whole is a judgement.
Sum and Product Types
Products
Basic Programming Language Theory
Total Programming Language