file.pdf (142.05 kB)

How to Believe a Twelf Proof

Download (142.05 kB)
journal contribution
posted on 01.08.1998, 00:00 by Robert Harper, Karl Crary
Logical systems are represented in LF by giving a full and faithful (adequate) embedding of the deductive apparatus of the logic as canonical forms of certain types and kinds in LF in specified contexts. The collection of contexts over which the representation is adequate is called a world, because it provides generators for the canonical forms in question. Transferring adequacy from one world to another relies on the concept of subordination, which expresses the irrelevance of any “extra” variables in the target world.

History

Date

01/08/1998

Exports

Exports