## Proof of Type Soundness Using Logical Relation

2024-06-05This blog compares proving type soundness using traditional progress/preservation methods and logical relations^{1}. Credits go to the original author of these ideas.

## Note for Constructive Logic

2024-05-08This is a note for my learning of Constructive Logic by **Frank Pfenning**. Logic is the study of the principles of valid inferences and demonstration, which constitutes an important area in the disciplines of philosophy and mathematics.

## From Turing Machine to Lambda Calculus

2024-05-04In the past first semester of my Ph.D. in computer science, my attention was attracted by the study of Alonzo Church and Alan Turing, specifically, the Turing Machine developed by Alan Turing in 1936, and the lambda calculus developed by Alonzo Church in 1930, which turns out to be Turing complete and is equivalent in omputational power with Turing Machine.