Kripke Semantics for a Logical Framework

Alex Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a semantics (using Kripke lambda models) for a logical framework (minimal implicational predicate logic with quantification over all higher types). We apply the semantics to obtain straightforward adequacy proofs for encodings of logics in the framework. 1 Introduction There has been much recent interest in the development and use of logical frameworks. A logical framework is a formal system within which many different logics can be easily represented. It is hoped that such frameworks will facilitate the rapid development of proof assistants for the wide variety of different logics used in computer science and other fields. In this paper we give a semantic analysis (using Kripke lambda models) of the use of minimal implicational predicate logic (with quantification over all higher types) as a logical framework. We choose this framework because it is relatively straightforward to give it a useful semantics. The use of such a logic as a framework is not new.
Original languageEnglish
Title of host publicationWorkshop on Types for Proofs and Programs
Number of pages36
Publication statusPublished - 1993

Fingerprint

Dive into the research topics of 'Kripke Semantics for a Logical Framework'. Together they form a unique fingerprint.

Cite this