Parametricity - Logical Equivalence for Polymorphic Types

Hereditary Termination and Logical Equivalence Recap

Polymorphic Functional Programming

An example to start off

In Searching Counter Examples for Ramsey Number

This is a project I did in my undergrad, so I might forget some of the details. Also some of the design choices might seen stupid for now, but I am writing t...

Introduction

Introduction to Category Theory

We can think of category theory as a generalized set theory, where in set theory we have sets and $\in$, but in category theory we have objects and arrows, w...

Equational Reasoning

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

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

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.