Concept lattices and similarity in non-commutative fuzzy logic. - George Georgescu; Andrei Popescu 001 (Fundam. Informaticae, 2002)

Non-commutative fuzzy Galois connections. - George Georgescu; Andrei Popescu 001 (Soft Comput., 2003)

Non-dual fuzzy connections. - George Georgescu; Andrei Popescu 001 (Arch. Math. Log., 2004)

Non-commutative fuzzy structures and pairs of weak negations. - George Georgescu; Andrei Popescu 001 (Fuzzy Sets Syst., 2004)

Languages Generated Using an Abstract Catenation. - Andrei Popescu 001 (Grammars, 2004)

A general approach to fuzzy concepts. - Andrei Popescu 001 (Math. Log. Q., 2004)

Behavioral Extensions of Institutions. - Andrei Popescu 001; Grigore Rosu (CALCO, 2005)

Similarity Convergence in Residuated Structures. - George Georgescu; Andrei Popescu 001 (Log. J. IGPL, 2005)

Lukasiewicz-Moisil Relation Algebras. - Andrei Popescu 001 (Stud Logica, 2005)

A common generalization for MV-algebras and Lukasiewicz-Moisil algebras. - George Georgescu; Andrei Popescu 001 (Arch. Math. Log., 2006)

An Institution-independent Generalization of Tarski's Elementary Chain Theorem. - Daniel Gâinâ; Andrei Popescu 001 (J. Log. Comput., 2006)

Order Convergence and Distance on Lukasiewicz-Moisil Algebras. - George Geordesce; Ioana Leustean; Andrei Popescu 001 (J. Multiple Valued Log. Soft Comput., 2006)

A New Class of Probabilities on Lukasiewicz-Moisil Algebras. - George Georgescu; Andrei Popescu 001 (J. Multiple Valued Log. Soft Comput., 2006)

An Institution-Independent Proof of the Robinson Consistency Theorem. - Daniel Gâinâ; Andrei Popescu 001 (Stud Logica, 2007)

Weak Bisimilarity Coalgebraically. - Andrei Popescu 001 (CALCO, 2009)

Theory support for weak higher order abstract syntax in Isabelle/HOL. - Elsa L. Gunter; Christopher J. Osborn; Andrei Popescu 001 (LFMTP, 2009)

Ordinals and Cardinals. - Andrei Popescu 001 (Arch. Formal Proofs, 2009)

A semantic approach to interpolation. - Andrei Popescu 001; Traian-Florin Serbanuta; Grigore Rosu (Theor. Comput. Sci., 2009)

Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. - Andrei Popescu 001; Elsa L. Gunter (FoSSaCS, 2010)

Strong Normalization for System F by HOAS on Top of FOAS. - Andrei Popescu 001; Elsa L. Gunter; Christopher J. Osborn (LICS, 2010)

Contributions to the theory of syntax with bindings and to process algebra - Andrei Popescu 001 (2010)

Recursion principles for syntax with bindings and substitution. - Andrei Popescu 001; Elsa L. Gunter (ICFP, 2011)

Proving Concurrent Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (CPP, 2012)

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. - Jasmin Christian Blanchette; Andrei Popescu 001; Daniel Wand; Christoph Weidenbach (ITP, 2012)

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. - Dmitriy Traytel; Andrei Popescu 001; Jasmin Christian Blanchette (LICS, 2012)

Possibilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl (Arch. Formal Proofs, 2012)

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (CALCO, 2013)

Formalizing Probabilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (CPP, 2013)

Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. - Andreas Schropp; Andrei Popescu 001 (CPP, 2013)

Mechanizing the Metatheory of Sledgehammer. - Jasmin Christian Blanchette; Andrei Popescu 001 (FroCos, 2013)

Sound and Complete Sort Encodings for First-Order Logic. - Jasmin Christian Blanchette; Andrei Popescu 001 (Arch. Formal Proofs, 2013)

Security Type Systems as Recursive Predicates. - Andrei Popescu 001 (CoRR, 2013)

Formal Verification of Language-Based Concurrent Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (J. Formaliz. Reason., 2013)

Unified Classical Logic Completeness - A Coinductive Pearl. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (IJCAR, 2014)

A Conference Management System with Verified Document Confidentiality. - Sudeep Kanav; Peter Lammich; Andrei Popescu 001 (CAV, 2014)

Cardinals in Isabelle/HOL. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (ITP, 2014)

Truly Modular (Co)datatypes for Isabelle/HOL. - Jasmin Christian Blanchette; Johannes Hölzl; Andreas Lochbihler; Lorenz Panny; Andrei Popescu 001; Dmitriy Traytel (ITP, 2014)

Probabilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl (Arch. Formal Proofs, 2014)

Abstract Completeness. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2014)

Bounded-Deducibility Security. - Andrei Popescu 001; Peter Lammich (Arch. Formal Proofs, 2014)

A shallow embedding of HyperCTL. - Markus N. Rabe; Peter Lammich; Andrei Popescu 001 (Arch. Formal Proofs, 2014)

Making security type systems less ad hoc. - Tobias Nipkow; Andrei Popescu 001 (it Inf. Technol., 2014)

Witnessing (Co)datatypes. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (ESOP, 2015)

Foundational extensible corecursion: a proof assistant perspective. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (ICFP, 2015)

Foundational Extensible Corecursion. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (CoRR, 2015)

Term-generic logic. - Andrei Popescu 001; Grigore Rosu (Theor. Comput. Sci., 2015)

From Types to Sets by Local Type Definitions in Higher-Order Logic. - Ondrej Kuncar; Andrei Popescu 001 (ITP, 2016)

Encoding Monomorphic and Polymorphic Types. - Jasmin Christian Blanchette; Sascha Böhme; Andrei Popescu 001; Nicholas Smallbone (Log. Methods Comput. Sci., 2016)

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. - Jasmin Christian Blanchette; Aymeric Bouzy; Andreas Lochbihler; Andrei Popescu 001; Dmitriy Traytel (ESOP, 2017)

Comprehending Isabelle/HOL's Consistency. - Ondrej Kuncar; Andrei Popescu 001 (ESOP, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

A Formalized General Theory of Syntax with Bindings. - Lorenzo Gheri; Andrei Popescu 001 (ITP, 2017)

Foundational nonuniform (Co)datatypes for higher-order logic. - Jasmin Christian Blanchette; Fabian Meier; Andrei Popescu 001; Dmitriy Traytel (LICS, 2017)

CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. - Thomas Bauereiß; Armando Pesenti Gritti; Andrei Popescu 001; Franco Raimondi (IEEE Symposium on Security and Privacy, 2017)

Abstract Soundness. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2017)

Operations on Bounded Natural Functors. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2017)

Soundness and Completeness Proofs by Coinductive Methods. - Jasmin Christian Blanchette; Andrei Popescu 001; Dmitriy Traytel (J. Autom. Reason., 2017)

Introduction to Milestones in Interactive Theorem Proving. - Jeremy Avigad; Jasmin Christian Blanchette; Gerwin Klein; Lawrence C. Paulson; Andrei Popescu 001; Gregor Snelting (J. Autom. Reason., 2018)

CoSMed: A Confidentiality-Verified Social Media Platform. - Thomas Bauereiß; Armando Pesenti Gritti; Andrei Popescu 001; Franco Raimondi (J. Autom. Reason., 2018)

Safety and conservativity of definitions in HOL and Isabelle/HOL. - Ondrej Kuncar; Andrei Popescu 001 (Proc. ACM Program. Lang., 2018)

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. - Andrei Popescu 001; Dmitriy Traytel (CADE, 2019)

A General Theory of Syntax with Bindings. - Lorenzo Gheri; Andrei Popescu 001 (Arch. Formal Proofs, 2019)

From Types to Sets by Local Type Definition in Higher-Order Logic. - Ondrej Kuncar; Andrei Popescu 001 (J. Autom. Reason., 2019)

A Consistent Foundation for Isabelle/HOL. - Ondrej Kuncar; Andrei Popescu 001 (J. Autom. Reason., 2019)

Bindings as bounded natural functors. - Jasmin Christian Blanchette; Lorenzo Gheri; Andrei Popescu 001; Dmitriy Traytel (Proc. ACM Program. Lang., 2019)

From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. - Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2020)

From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. - Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2020)

An Abstract Formalization of Gödel's Incompleteness Theorems. - Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2020)

Robinson Arithmetic. - Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2020)

Syntax-Independent Logic Infrastructure. - Andrei Popescu 001; Dmitriy Traytel (Arch. Formal Proofs, 2020)

A Formalized General Theory of Syntax with Bindings: Extended Version. - Lorenzo Gheri; Andrei Popescu 001 (J. Autom. Reason., 2020)

Bounded-Deducibility Security (Invited Paper). - Andrei Popescu 001; Thomas Bauereiss; Peter Lammich (ITP, 2021)

Compositional BD Security. - Thomas Bauereiss; Andrei Popescu 001 (Arch. Formal Proofs, 2021)

CoSMeDis: A confidentiality-verified distributed social media platform. - Thomas Bauereiss; Andrei Popescu 001 (Arch. Formal Proofs, 2021)

CoSMed: A confidentiality-verified social media platform. - Thomas Bauereiss; Andrei Popescu 001 (Arch. Formal Proofs, 2021)

Fresh identifiers. - Andrei Popescu 001; Thomas Bauereiss (Arch. Formal Proofs, 2021)

CoCon: A Confidentiality-Verified Conference Management System. - Andrei Popescu 001; Peter Lammich; Thomas Bauereiss (Arch. Formal Proofs, 2021)

Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS. - Lorenzo Gheri; Andrei Popescu 001 (CoRR, 2021)

Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. - Andrei Popescu 001; Dmitriy Traytel (J. Autom. Reason., 2021)

CoCon: A Conference Management System with Formally Verified Document Confidentiality. - Andrei Popescu 001; Peter Lammich; Ping Hou (J. Autom. Reason., 2021)

Rensets and Renaming-Based Recursion for Syntax with Bindings. - Andrei Popescu 001 (IJCAR, 2022)

A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress). - Artur Graczyk; Marialena Hadjikosti; Andrei Popescu 001 (iFM, 2023)

Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion. - Andrei Popescu 001 (Arch. Formal Proofs, 2023)

Admissible Types-to-PERs Relativization in Higher-Order Logic. - Andrei Popescu 001; Dmitriy Traytel (Proc. ACM Program. Lang., 2023)

Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version. - Andrei Popescu 001 (J. Autom. Reason., 2023)

Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. - Brijesh Dongol; Matt Griffin; Andrei Popescu 001; Jamie Wright (CSF, 2024)

Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress). - Gergely Buday; Andrei Popescu 001 (PhD@IFM, 2024)

Countable Sums and Discrete (Sub)Distributions. - Gergely Buday; Andrei Popescu 001 (Arch. Formal Proofs, 2024)

Secret-Directed Unwinding. - Brijesh Dongol; Matthew Griffin; Andrei Popescu 001; Jamie Wright (Arch. Formal Proofs, 2024)

More Operations on Lazy Lists. - Andrei Popescu 001; Jamie Wright (Arch. Formal Proofs, 2024)

Relative Security. - Andrei Popescu 001; Jamie Wright (Arch. Formal Proofs, 2024)

A formalized programming language with speculative execution. - Jamie Wright; Andrei Popescu 001 (Arch. Formal Proofs, 2024)

The Complex(ity) Landscape of Checking Infinite Descent. - Liron Cohen 001; Adham Jabarin; Andrei Popescu 001; Reuben N. S. Rowe (Proc. ACM Program. Lang., 2024)

Nominal Recursors as Epi-Recursors. - Andrei Popescu 001 (Proc. ACM Program. Lang., 2024)

Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. - Jan van Brügge; James McKinna; Andrei Popescu 001; Dmitriy Traytel (Proc. ACM Program. Lang., 2025)