1 citations · 1 across the 5 of their papers we have counts for
5 papers · 1 filter
Justification Logic of the Lambda Calculus
Silvia Ghilezan, Paaras Padhiar
The simply typed λ-calculus is a model of computation where typed terms correspond to proofs of intuitionistic propositional logic (IPL) via the Curry-Howard correspondence. Justif…
Intuitionistic Justification Logic, Semantically
Sonia Marin, Paaras Padhiar, Ian Shillito
Justification logics are explicit versions of modal logic. In the classical setting, this means boxes are refined with explicit proof terms and interact with each other through pro…
The proof theory and semantics of second-order (intuitionistic) tense logic
Justus Becker, Anupam Das, Sonia Marin +1
We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order log…
Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
Sonia Marin, Paaras Padhiar
Justification logics are an explication of modal logic; boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-fr…
Nested Sequents for Quasi-transitive Modal Logics
Sonia Marin, Paaras Padhiar
Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent.…