Extending a Logical Framework with a Modal Connective for Validity

Matthews, Seán

doi:10.1007/BFb0014564

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Extending a Logical Framework with a Modal Connective for Validity

MPS-Authors

/persons/resource/persons45002

Matthews, Seán
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

https://rdcu.be/dwqAI
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Matthews, S. (1997). Extending a Logical Framework with a Modal Connective for Validity. In M. Abadi, & T. Ito (Eds.), Theoretical Aspects of Computer Software (pp. 491-514). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-39DE-D

Abstract

Logical frameworks, formal systems for programming consequence based proof
systems, are well known. The notations that have been proposed are
suited best to natural deduction style presentations based on truth
consequence. We develop a conservative extension of a typical logical
framework providing a modal connective which we can use to formalise
validity. We argue that this extension is sensible, and provide
example encodings of non-standard logics in its terms.