Programming Languages

Equational Reasoning

2 minute read

The main question is, how do we define two programs are equal, and how do we prove it.

Type Theory Foundations

3 minute read

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...

Computational Interpretations

2 minute read

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

1 minute read

We state “A is true”, then “A” is a proposition, and “A is true” as a whole is a judgement.