Distributed System Security via Logical Frameworks
Software Implementations
Formalization of noninterference in constructive authorization logic
A formalization of constructive authorization logics and some metatheorems about it in Twelf.
Propositional prover:
A theorem prover for propositional intuitionistic linear logic based on the inverse method using focusing. The prover is described in [CADE20]
with more of its foundation in [CSL'05]. It further contains direct
support for affine logic and lax logic.
Firstorder prover:
A theorem prover for firstorder intuitionistic linear logic based on the inverse method using focusing. The prover is described in [CADE20]. It further contains direct support for affine logic and lax logic.
LolliMon:
A linear logic programming language that combines forward and backward
reasoning. Backward reasoning backtracks as usual in Prolog, while
forward chaining provides support for committed choice concurrency
and saturation. The language design is described in [PPDP'05].
 Lollimon (last updated: Mon Jul 11 2005)
[ Home
 Publications
 Software  Links
]
