Directly Indecomposables in Semidegenerate Varieties of Connected po-Groupoids. - Pedro Sánchez Terraf (Order, 2008)

Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization. - Pedro R. D'Argenio; Nicolás Wolovick; Pedro Sánchez Terraf; Pablo Celayes (QEST, 2009)

Bisimulations for Nondeterministic Labeled Markov Processes - Pedro R. D'Argenio; Pedro Sánchez Terraf; Nicolás Wolovick (CoRR, 2010)

Unprovability of the logical characterization of bisimulation. - Pedro Sánchez Terraf (Inf. Comput., 2011)

Boolean factor Congruences and Property (*). - Pedro Sánchez Terraf (Int. J. Algebra Comput., 2011)

A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems. - Carlos E. Budde; Pedro R. D'Argenio; Pedro Sánchez Terraf; Nicolás Wolovick (ROCKS, 2012)

Bisimulations for non-deterministic labelled Markov processes. - Pedro R. D'Argenio; Pedro Sánchez Terraf; Nicolás Wolovick (Math. Struct. Comput. Sci., 2012)

Stochastic Nondeterminism and Effectivity Functions. - Ernst-Erich Doberkat; Pedro Sánchez Terraf (CoRR, 2014)

The Lattice of Congruences of a Finite Linear Frame. - Carlos Areces; Miguel Campercholi; Daniel Penazzi; Pedro Sánchez Terraf (CoRR, 2015)

The lattice of congruences of a finite line frame. - Carlos Areces; Miguel Campercholi; Daniel Penazzi; Pedro Sánchez Terraf (J. Log. Comput., 2017)

Stochastic non-determinism and effectivity functions. - Ernst-Erich Doberkat; Pedro Sánchez Terraf (J. Log. Comput., 2017)

Bisimilarity is not Borel. - Pedro Sánchez Terraf (Math. Struct. Comput. Sci., 2017)

First Steps Towards a Formalization of Forcing. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf (LSFA, 2018)

Mechanization of Separation in Generic Extensions. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf (CoRR, 2019)

Formalization of Forcing in Isabelle/ZF. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf (Arch. Formal Proofs, 2020)

Cofinality and the Delta System Lemma. - Pedro Sánchez Terraf (Arch. Formal Proofs, 2020)

Semipullbacks of labelled Markov processes. - Jan Pachl; Pedro Sánchez Terraf (Log. Methods Comput. Sci., 2021)

Transitive Models of Fragments of ZFC. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Arch. Formal Proofs, 2022)

The Independence of the Continuum Hypothesis in Isabelle/ZF. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Arch. Formal Proofs, 2022)

The Zhou Ordinal of Labelled Markov Processes over separable Spaces. - Martín Santiago Moroni; Pedro Sánchez Terraf (Rev. Symb. Log., 2023)

The formal verification of the ctm approach to forcing. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Ann. Pure Appl. Log., 2024)

A classification of bisimilarities for general Markov decision processes. - Martín Santiago Moroni; Pedro Sánchez Terraf (Math. Struct. Comput. Sci., 2025)