Andrei Popescu

111 papers A* 6A 10B 21Journal 66Unranked 6

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction -. ESOP (1) John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright
2025	B	`conf`	Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. ITP Jan van Brügge, Andrei Popescu, Dmitriy Traytel
2025	J	`jnl`	Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. Proc. ACM Program. Lang. Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel
2025	A*	`conf`	Completing Gordon's Higher-Order Logic. LICS Andrei Popescu
2025	J	`jnl`	Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL. J. Autom. Reason. John Derrick, Brijesh Dongol, Chelsea Edmonds, Matt Griffin, Andrei Popescu, Jamie Wright
2024	J	`jnl`	A formalized programming language with speculative execution. Arch. Formal Proofs Jamie Wright, Andrei Popescu
2024	J	`jnl`	Countable Sums and Discrete (Sub)Distributions. Arch. Formal Proofs Gergely Buday, Andrei Popescu
2024	—	`conf`	Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress). PhD@IFM Gergely Buday, Andrei Popescu
2024	J	`jnl`	More Operations on Lazy Lists. Arch. Formal Proofs Andrei Popescu, Jamie Wright
2024	J	`jnl`	Nominal Recursors as Epi-Recursors. Proc. ACM Program. Lang. Andrei Popescu
2024	J	`jnl`	Relative Security. Arch. Formal Proofs Andrei Popescu, Jamie Wright
2024	A	`conf`	Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. CSF Brijesh Dongol, Matt Griffin, Andrei Popescu, Jamie Wright
2024	J	`jnl`	Secret-Directed Unwinding. Arch. Formal Proofs Brijesh Dongol, Matthew Griffin, Andrei Popescu, Jamie Wright
2024	J	`jnl`	The Complex(ity) Landscape of Checking Infinite Descent. Proc. ACM Program. Lang. Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe
2023	B	`conf`	A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress). iFM Artur Graczyk, Marialena Hadjikosti, Andrei Popescu
2023	J	`jnl`	Admissible Types-to-PERs Relativization in Higher-Order Logic. Proc. ACM Program. Lang. Andrei Popescu, Dmitriy Traytel
2023	J	`jnl`	Nominal Recursors as Epi-Recursors. CoRR Andrei Popescu
2023	J	`jnl`	Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion. Arch. Formal Proofs Andrei Popescu
2023	J	`jnl`	Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version. J. Autom. Reason. Andrei Popescu
2022	B	`ed.`	CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 CPP Andrei Popescu, Steve Zdancewic
2022	A	`conf`	Rensets and Renaming-Based Recursion for Syntax with Bindings. IJCAR Andrei Popescu
2022	J	`jnl`	Rensets and Renaming-Based Recursion for Syntax with Bindings. CoRR Andrei Popescu
2021	B	`conf`	Bounded-Deducibility Security (Invited Paper). ITP Andrei Popescu, Thomas Bauereiss, Peter Lammich
2021	B	`ed.`	CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021 CPP Catalin Hritcu, Andrei Popescu
2021	J	`jnl`	Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS. CoRR Lorenzo Gheri, Andrei Popescu
2021	J	`jnl`	CoCon: A Conference Management System with Formally Verified Document Confidentiality. J. Autom. Reason. Andrei Popescu, Peter Lammich, Ping Hou
2021	J	`jnl`	CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs Andrei Popescu, Peter Lammich, Thomas Bauereiss
2021	J	`jnl`	CoSMeDis: A confidentiality-verified distributed social media platform. Arch. Formal Proofs Thomas Bauereiss, Andrei Popescu
2021	J	`jnl`	CoSMed: A confidentiality-verified social media platform. Arch. Formal Proofs Thomas Bauereiss, Andrei Popescu
2021	J	`jnl`	Compositional BD Security. Arch. Formal Proofs Thomas Bauereiss, Andrei Popescu
2021	J	`jnl`	Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. J. Autom. Reason. Andrei Popescu, Dmitriy Traytel
2021	J	`jnl`	Fresh identifiers. Arch. Formal Proofs Andrei Popescu, Thomas Bauereiss
2020	J	`jnl`	A Formalized General Theory of Syntax with Bindings: Extended Version. J. Autom. Reason. Lorenzo Gheri, Andrei Popescu
2020	J	`jnl`	An Abstract Formalization of Gödel's Incompleteness Theorems. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	Robinson Arithmetic. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	Syntax-Independent Logic Infrastructure. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2019	J	`jnl`	A Consistent Foundation for Isabelle/HOL. J. Autom. Reason. Ondrej Kuncar, Andrei Popescu
2019	A	`conf`	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. CADE Andrei Popescu, Dmitriy Traytel
2019	J	`jnl`	A General Theory of Syntax with Bindings. Arch. Formal Proofs Lorenzo Gheri, Andrei Popescu
2019	B	`ed.`	Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings TABLEAUX Serenella Cerrito, Andrei Popescu
2019	J	`jnl`	Bindings as bounded natural functors. Proc. ACM Program. Lang. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
2019	J	`jnl`	From Types to Sets by Local Type Definition in Higher-Order Logic. J. Autom. Reason. Ondrej Kuncar, Andrei Popescu
2019	—	`ed.`	Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings FroCoS Andreas Herzig, Andrei Popescu
2018	J	`jnl`	CoSMed: A Confidentiality-Verified Social Media Platform. J. Autom. Reason. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
2018	J	`jnl`	Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
2018	J	`jnl`	Safety and conservativity of definitions in HOL and Isabelle/HOL. Proc. ACM Program. Lang. Ondrej Kuncar, Andrei Popescu
2017	B	`conf`	A Formalized General Theory of Syntax with Bindings. ITP Lorenzo Gheri, Andrei Popescu
2017	J	`jnl`	A Formalized General Theory of Syntax with Bindings. CoRR Lorenzo Gheri, Andrei Popescu
2017	J	`jnl`	Abstract Soundness. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2017	A*	`conf`	CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. IEEE Symposium on Security and Privacy Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
2017	A	`conf`	Comprehending Isabelle/HOL's Consistency. ESOP Ondrej Kuncar, Andrei Popescu
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
2017	A*	`conf`	Foundational nonuniform (Co)datatypes for higher-order logic. LICS Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
2017	A	`conf`	Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
2017	J	`jnl`	Operations on Bounded Natural Functors. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2017	J	`jnl`	Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2016	B	`conf`	CoSMed: A Confidentiality-Verified Social Media Platform. ITP Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
2016	J	`jnl`	Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
2016	B	`conf`	From Types to Sets by Local Type Definitions in Higher-Order Logic. ITP Ondrej Kuncar, Andrei Popescu
2015	B	`conf`	A Consistent Foundation for Isabelle/HOL. ITP Ondrej Kuncar, Andrei Popescu
2015	J	`jnl`	Foundational Extensible Corecursion. CoRR Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2015	A	`conf`	Foundational extensible corecursion: a proof assistant perspective. ICFP Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2015	J	`jnl`	Term-generic logic. Theor. Comput. Sci. Andrei Popescu, Grigore Rosu
2015	A	`conf`	Witnessing (Co)datatypes. ESOP Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	A*	`conf`	A Conference Management System with Verified Document Confidentiality. CAV Sudeep Kanav, Peter Lammich, Andrei Popescu
2014	J	`jnl`	A shallow embedding of HyperCTL. Arch. Formal Proofs Markus N. Rabe, Peter Lammich, Andrei Popescu
2014	J	`jnl`	Abstract Completeness. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	J	`jnl`	Bounded-Deducibility Security. Arch. Formal Proofs Andrei Popescu, Peter Lammich
2014	B	`conf`	Cardinals in Isabelle/HOL. ITP Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	J	`jnl`	Making security type systems less ad hoc. it Inf. Technol. Tobias Nipkow, Andrei Popescu
2014	J	`jnl`	Probabilistic Noninterference. Arch. Formal Proofs Andrei Popescu, Johannes Hölzl
2014	B	`conf`	Truly Modular (Co)datatypes for Isabelle/HOL. ITP Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
2014	A	`conf`	Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2013	A	`conf`	Encoding Monomorphic and Polymorphic Types. TACAS Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
2013	J	`jnl`	Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	B	`conf`	Formalizing Probabilistic Noninterference. CPP Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	—	`conf`	Mechanizing the Metatheory of Sledgehammer. FroCos Jasmin Christian Blanchette, Andrei Popescu
2013	B	`conf`	Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. CPP Andreas Schropp, Andrei Popescu
2013	B	`conf`	Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	J	`jnl`	Security Type Systems as Recursive Predicates. CoRR Andrei Popescu
2013	J	`jnl`	Sound and Complete Sort Encodings for First-Order Logic. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu
2012	A*	`conf`	Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
2012	B	`conf`	More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
2012	J	`jnl`	Possibilistic Noninterference. Arch. Formal Proofs Andrei Popescu, Johannes Hölzl
2012	B	`conf`	Proving Concurrent Noninterference. CPP Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2011	A	`conf`	Recursion principles for syntax with bindings and substitution. ICFP Andrei Popescu, Elsa L. Gunter
2010	—	`—`	Contributions to the theory of syntax with bindings and to process algebra Andrei Popescu
2010	B	`conf`	Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. FoSSaCS Andrei Popescu, Elsa L. Gunter
2010	A*	`conf`	Strong Normalization for System F by HOAS on Top of FOAS. LICS Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn
2009	J	`jnl`	A semantic approach to interpolation. Theor. Comput. Sci. Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu
2009	J	`jnl`	Ordinals and Cardinals. Arch. Formal Proofs Andrei Popescu
2009	—	`conf`	Theory support for weak higher order abstract syntax in Isabelle/HOL. LFMTP Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu
2009	B	`conf`	Weak Bisimilarity Coalgebraically. CALCO Andrei Popescu
2008	—	`conf`	Term-Generic Logic. WADT Andrei Popescu, Grigore Rosu
2007	J	`jnl`	An Institution-Independent Proof of the Robinson Consistency Theorem. Stud Logica Daniel Gâinâ, Andrei Popescu
2006	J	`jnl`	A New Class of Probabilities on Lukasiewicz-Moisil Algebras. J. Multiple Valued Log. Soft Comput. George Georgescu, Andrei Popescu
2006	B	`conf`	A Semantic Approach to Interpolation. FoSSaCS Andrei Popescu, Traian Serbanuta, Grigore Rosu
2006	J	`jnl`	A common generalization for MV-algebras and Lukasiewicz-Moisil algebras. Arch. Math. Log. George Georgescu, Andrei Popescu
2006	J	`jnl`	An Institution-independent Generalization of Tarski's Elementary Chain Theorem. J. Log. Comput. Daniel Gâinâ, Andrei Popescu
2006	J	`jnl`	Order Convergence and Distance on Lukasiewicz-Moisil Algebras. J. Multiple Valued Log. Soft Comput. George Geordesce, Ioana Leustean, Andrei Popescu
2005	B	`conf`	Behavioral Extensions of Institutions. CALCO Andrei Popescu, Grigore Rosu
2005	J	`jnl`	Lukasiewicz-Moisil Relation Algebras. Stud Logica Andrei Popescu
2005	J	`jnl`	Similarity Convergence in Residuated Structures. Log. J. IGPL George Georgescu, Andrei Popescu
2004	J	`jnl`	A general approach to fuzzy concepts. Math. Log. Q. Andrei Popescu
2004	J	`jnl`	Languages Generated Using an Abstract Catenation. Grammars Andrei Popescu
2004	J	`jnl`	Non-commutative fuzzy structures and pairs of weak negations. Fuzzy Sets Syst. George Georgescu, Andrei Popescu
2004	J	`jnl`	Non-dual fuzzy connections. Arch. Math. Log. George Georgescu, Andrei Popescu
2003	J	`jnl`	Non-commutative fuzzy Galois connections. Soft Comput. George Georgescu, Andrei Popescu
2002	J	`jnl`	Concept lattices and similarity in non-commutative fuzzy logic. Fundam. Informaticae George Georgescu, Andrei Popescu