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

Citations by Year