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. ...
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan: (\mathrmLF^+) in \textttCoqfor fast-and-loose reasoning (2019)
- Rabe, Florian: A modular type reconstruction algorithm (2018)
- Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: (\mathsfLLF_\mathcalP): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
- Honsell, Furio; Lenisa, Marina; Liquori, Luigi; Scagnetto, Ivan: Implementing Cantor’s paradise (2016)