A Simple Theory of Expressions, Judgments and Derivations

We propose a simple theory of expressions which is intended to be used as a foundational syntactic structure for the Natural Framework (NF). We define expression formally and give a simple proof of the decidability of α-equivalence. We use this new theory of expressions to define judgments and derivations formally, and we give concrete examples of derivation games to show a flavor of NF.

• Type: Conference
• Year: 2004
• Where: ASIAN
• Authors: Masahiko Sato
• Keywords: ASIAN 2004, Foundational Syntactic Structure, Simple Proof, Simple Theory