$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

DOI10.23638/LMCS-13(3:2)2017zbMath1456.03027arXiv1702.07214OpenAlexW2591697020MaRDI QIDQ5278085

Petar Maksimović, Furio Honsell, Ivan Scagnetto, Luigi Liquori

Publication date: 13 July 2017

Full work available at URL: https://arxiv.org/abs/1702.07214

zbMATH Keywords

type theorytyped lambda calculuslogical frameworkscomputer-aided formal verfication

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Related Items (3)

LF+ in Coq for "fast and loose" reasoning ⋮ Implementing Cantor’s Paradise ⋮ LLFp

Uses Software

• Beluga
• Twelf
• Automath

This page was built for publication: $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads