LLFp swMATH ID: 20866 Software Authors: Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan Description: LLFp: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. We extend the constructive dependent type theory of the Logical Framework 𝖫𝖥 with monadic, dependent type constructors indexed with predicates over judgements, called Locks. ... Homepage: https://arxiv.org/pdf/1702.07214.pdf Keywords: computer aided formal verfication; type theory; logical frameworks; typed lambda calculus Related Software: Coq; MMT; Agda; Beluga; Twelf; GitHub; ELPI; Delphin; LATIN; HOLyHammer; Abella; Isar; PVS; Isabelle; Automath Cited in: 4 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Zbl 1456.03027Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan 2017 all top 5 Cited by 9 Authors 3 Honsell, Furio 3 Scagnetto, Ivan 2 Lenisa, Marina 2 Liquori, Luigi 1 Alessi, Fabio 1 Ciaffaglione, Alberto 1 Di Gianantonio, Pietro 1 Maksimović, Petar 1 Rabe, Florian Cited in 3 Serials 1 ACM Transactions on Computational Logic 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning Cited in 2 Fields 3 Mathematical logic and foundations (03-XX) 3 Computer science (68-XX) Citations by Year