LLFp

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

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 4 articles , 1 standard article )

Showing results 1 to 4 of 4.
Sorted by year (citations)

  1. Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan: (\mathrmLF^+) in \textttCoqfor fast-and-loose reasoning (2019)
  2. Rabe, Florian: A modular type reconstruction algorithm (2018)
  3. 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)
  4. Honsell, Furio; Lenisa, Marina; Liquori, Luigi; Scagnetto, Ivan: Implementing Cantor’s paradise (2016)