LF+ in Coq for "fast and loose" reasoning

LF+ in Coq for "fast and loose" reasoning

We develop the metatheory and the implementation of LF+, and discuss several applications. LF+ capitalizes on research work, carried out by the authors over more than a decade, on Logical Frameworks. It builds on various conservative extensions of LF, which feature "lock"-type constructors...

Full description

Bibliographic Details
Main Authors: Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto
Format: Article
Language:English
Published: University of Bologna 2019-12-01
Series:Journal of Formalized Reasoning
Subjects:
type theory
logical frameworks
computer aided formal reasoning
Online Access:https://jfr.unibo.it/article/view/9757

Internet

https://jfr.unibo.it/article/view/9757

Similar Items