How to prove it in Natural Deduction: A Tactical Approach. - Favio Ezequiel Miranda-Perea; P. Selene Linares-Arévalo; Atocha Aliseda-Llera (CoRR, 2015)

On interactive proof-search for constructive modal necessity. - Favio Ezequiel Miranda-Perea; Lourdes Del Carmen González-Huesca; P. Selene Linares-Arévalo (LANMR, 2019)

Dual and Axiomatic Systems for Constructive S4, a Formally Verified Equivalence. - Lourdes Del Carmen González-Huesca; Favio Ezequiel Miranda-Perea; P. Selene Linares-Arévalo (LSFA, 2019)

Axiomatic and dual systems for constructive necessity, a formally verified equivalence. - Lourdes Del Carmen González-Huesca; Favio Ezequiel Miranda-Perea; P. Selene Linares-Arévalo (J. Appl. Non Class. Logics, 2019)

Composing Linear Types and Separation Logic Proofs of Memory Safety. - Pilar Selene Linares-Arévalo (SPLASH Companion, 2022)

A dual-context sequent calculus for the constructive modal logic S4. - Favio Ezequiel Miranda-Perea; Lourdes Del Carmen González-Huesca; Pilar Selene Linares-Arévalo (Math. Struct. Comput. Sci., 2022)