Email Gateway (Nov 28 2024 at 15:55): Email Gateway (Nov 28 2024 at 15:55):From: Tobias Nipkow <nipkow@in.tum.de>
Deep Embedding of Intuitionistic Linear Logic
Filip Smola and Jacques D. Fleuriot
In this entry we formalise intuitionistic linear logic (ILL) with a deep
embedding of propositions, and shallow and deep embeddings of deductions. We
introduce the logic with an explicit exchange rule, meaning sequents have a list
of propositions as antecedents. We then prove that sequents that differ only in
the order of their antecedents are equivalently valid, representing the
alternative implicit exchange rule. The deep embedding of deductions allows for
direct construction, manipulation and verification of ILL deductions.
https://www.isa-afp.org/entries/ILL.html
Linear Resources and Process Compositions
Filip Smola and Jacques D. Fleuriot
In this entry we formalise a framework for process composition based on actions
that are specified by their input and output resources. We verify their
correctness by translating compositions of process into deductions of
intuitionistic linear logic. As part of the verification we derive simple
conditions on the compositions which ensure well-formedness of the corresponding
deduction.
We describe an earlier version of this formalisation in our article Linear
Resources in Isabelle/HOL, which also includes a formalisation of manufacturing
processes in the simulation game Factorio.
https://www.isa-afp.org/entries/ProcessComposition.html
Last updated: Jan 04 2025 at 20:18 UTC