Logical Frameworks--A Brief Introduction

A logical framework is a meta-language for the formalization of deductive systems. We provide a brief introduction to logical frameworks and their methodology, concentrating on LF. We use first-order logic as the running example to illustrate the representations of syntax, natural deductions, and proof transformations. We also sketch a recent formulation of LF centered on the notion of canonical form, and show how it affects proofs of adequacy of encodings.