Realizability for Monotone and Clausular (Co) inductive Definitions FE Miranda-Perea Electronic Notes in Theoretical Computer Science 123, 179-193, 2005 | 13 | 2005 |
Axiomatic and dual systems for constructive necessity, a formally verified equivalence LC González-Huesca, FE Miranda-Perea, PS Linares-Arévalo Journal of Applied Non-Classical Logics 29 (3), 255-287, 2019 | 7 | 2019 |
Incomparable families and maximal trees G Campero-Arena, J Cancino, M Hrušák, FE Miranda-Perea Fundamenta Mathematicae 234, 73-89, 2016 | 6 | 2016 |
How to prove it in natural deduction: A tactical approach FE Miranda-Perea, P Linares-Arévalo, A Aliseda 4th. International Conference on Tools for Teaching Logic, Rennes Francia, 9 …, 2015 | 6 | 2015 |
Some remarks on type systems for course-of-value recursion FE Miranda-Perea Electronic Notes in Theoretical Computer Science 247, 103-121, 2009 | 6 | 2009 |
Conjuntos y modelos: curso avanzado LMV Silva, DR Rebolledo, FEM Perea Universidad Autónoma Metropolitana, Unidad Iztapalapa, 2000 | 4 | 2000 |
Two extensions of system F with (co) iteration and primitive (co) recursion principles FE Miranda-Perea RAIRO-Theoretical Informatics and Applications 43 (4), 703-766, 2009 | 3 | 2009 |
On interactive proof-search for constructive modal necessity FE Miranda-Perea, LCG Huesca, PS Linares-Arévalo Electronic Notes in Theoretical Computer Science 354, 107-127, 2020 | 2 | 2020 |
Dual and Axiomatic Systems for Constructive S4, a Formally Verified Equivalence LC González-Huesca, FE Miranda-Perea, PS Linares-Arévalo Electronic Notes in Theoretical Computer Science 348, 61-83, 2020 | 2 | 2020 |
La lógica proposicional de segundo orden FEM PEREA Memorias 40, 1-31, 2009 | 2 | 2009 |
On extensions of AF2 with monotone and clausular (co) inductive definitions FE Miranda Perea Ludwig Maximillians Universitaet Muenchen, 2004 | 2 | 2004 |
Mendler-style Iso-(Co) inductive predicates: a strongly normalizing approach FE Miranda-Perea, LC González-Huesca Electronic Proceedings in Theoretical Computer Science 81, 2012 | 1 | 2012 |
A Curry-Style Realizability Interpretation for Monotone Inductive Definitions FE Miranda-Perea Proc. of 7th ESSLLI Student Session, ESSLLI, 155-166, 2002 | 1 | 2002 |
A Curry-style Realizability Interpretation for Monotone Inductive Definitions (Extended Version) FE Miranda-Perea Unpublished Draft, 2002 | 1 | 2002 |
On Conceptual changes in Computer Assisted Proofs FE Miranda Perea, LC González Huesca Almagest 14 (2), 222-245, 2023 | | 2023 |
Fitch-Style Modal Necessity as a Substructural Sequent-Style System FE Miranda-Perea, X Estrada Zavaleta, LC Gonzalez Huesca Computación y Sistemas 27 (1), 315-326, 2023 | | 2023 |
A dual-context sequent calculus for the constructive modal logic S4 FE Miranda-Perea, LCG Huesca, PSL Arévalo Mathematical Structures in Computer Science 32 (9), 1205-1233, 2022 | | 2022 |
A Dual-Context Sequent Calculus for S 4 Modal Lambda-Term Synthesis FE Miranda-Perea, S Omaña Silva, LC González Huesca Computación y Sistemas 26 (2), 787-799, 2022 | | 2022 |
On the Conciliation of Traditional and Computer-Assisted Proofs F E. Miranda-Perea, LCG Huesca Philosophy of Computing: Themes from IACAP 2019, 73-112, 2022 | | 2022 |
Interactive proof-search for equational reasoning FE Miranda-Perea, LC González Huesca, PS Linares-Arévalo Logic Journal of the IGPL 28 (6), 1155-1181, 2020 | | 2020 |