Syntax (Object logic)
From The Twelf Project
The syntax of an object logic is commonly encoded as an LF type family of kind type.
For example, if the language of our object logic is the natural numbers, its syntax would be declared in the following way.
declare a type family of kind "type" for natural numbers. nat : type. inhabit the nat with the appropriate constructors. nat/z : nat. nat/s : nat -> nat.
[edit] See also
- Read the introductions to Twelf to learn how to represent syntax in LF.
- Judgment
- Judgments as types
- Higher-order abstract syntax
This page is incomplete. We should expand it.
