Andrei Popescu

Publication Activity (10 Years)

Years Active: 2002-2024
Publications (10 Years): 45

Top Topics

Theorem Proving

Datalog Programs

Type Definitions

Top Venues

Arch. Formal Proofs

J. Autom. Reason.

Publications

Andrei Popescu
Nominal Recursors as Epi-Recursors. Proc. ACM Program. Lang. 8 (POPL) (2024)
Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe
The Complex(ity) Landscape of Checking Infinite Descent. Proc. ACM Program. Lang. 8 (POPL) (2024)
Andrei Popescu, Dmitriy Traytel
Admissible Types-to-PERs Relativization in Higher-Order Logic. Proc. ACM Program. Lang. 7 (POPL) (2023)
Andrei Popescu
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version. J. Autom. Reason. 67 (3) (2023)
Andrei Popescu
Nominal Recursors as Epi-Recursors. CoRR (2023)
Andrei Popescu
Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion. Arch. Formal Proofs 2023 (2023)
Artur Graczyk, Marialena Hadjikosti, Andrei Popescu
A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress). iFM (2023)
Andrei Popescu
Rensets and Renaming-Based Recursion for Syntax with Bindings. CoRR (2022)
Andrei Popescu
Rensets and Renaming-Based Recursion for Syntax with Bindings. IJCAR (2022)
Andrei Popescu, Thomas Bauereiss, Peter Lammich
Bounded-Deducibility Security (Invited Paper). ITP (2021)
Thomas Bauereiss, Andrei Popescu
CoSMed: A confidentiality-verified social media platform. Arch. Formal Proofs 2021 (2021)
Lorenzo Gheri, Andrei Popescu
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS. CoRR (2021)
Thomas Bauereiss, Andrei Popescu
Compositional BD Security. Arch. Formal Proofs 2021 (2021)
Andrei Popescu, Peter Lammich, Ping Hou
CoCon: A Conference Management System with Formally Verified Document Confidentiality. J. Autom. Reason. 65 (2) (2021)
Thomas Bauereiss, Andrei Popescu
CoSMeDis: A confidentiality-verified distributed social media platform. Arch. Formal Proofs 2021 (2021)
Andrei Popescu, Peter Lammich, Thomas Bauereiss
CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs 2021 (2021)
Andrei Popescu, Dmitriy Traytel
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. J. Autom. Reason. 65 (7) (2021)
Andrei Popescu, Thomas Bauereiss
Fresh identifiers. Arch. Formal Proofs 2021 (2021)
Andrei Popescu, Dmitriy Traytel
Robinson Arithmetic. Arch. Formal Proofs 2020 (2020)
Andrei Popescu, Dmitriy Traytel
From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. Arch. Formal Proofs 2020 (2020)
Andrei Popescu, Dmitriy Traytel
Syntax-Independent Logic Infrastructure. Arch. Formal Proofs 2020 (2020)
Lorenzo Gheri, Andrei Popescu
A Formalized General Theory of Syntax with Bindings: Extended Version. J. Autom. Reason. 64 (4) (2020)
Andrei Popescu, Dmitriy Traytel
An Abstract Formalization of Gödel's Incompleteness Theorems. Arch. Formal Proofs 2020 (2020)
Andrei Popescu, Dmitriy Traytel
From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. Arch. Formal Proofs 2020 (2020)
Ondrej Kuncar, Andrei Popescu
From Types to Sets by Local Type Definition in Higher-Order Logic. J. Autom. Reason. 62 (2) (2019)
Ondrej Kuncar, Andrei Popescu
A Consistent Foundation for Isabelle/HOL. J. Autom. Reason. 62 (4) (2019)
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3 (POPL) (2019)
Andrei Popescu, Dmitriy Traytel
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. CADE (2019)
Lorenzo Gheri, Andrei Popescu
A General Theory of Syntax with Bindings. Arch. Formal Proofs 2019 (2019)
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMed: A Confidentiality-Verified Social Media Platform. J. Autom. Reason. 61 (1-4) (2018)
Ondrej Kuncar, Andrei Popescu
Safety and conservativity of definitions in HOL and Isabelle/HOL. Proc. ACM Program. Lang. 2 (POPL) (2018)
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61 (1-4) (2018)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Abstract Soundness. Arch. Formal Proofs 2017 (2017)
Lorenzo Gheri, Andrei Popescu
A Formalized General Theory of Syntax with Bindings. ITP (2017)
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP (2017)
Lorenzo Gheri, Andrei Popescu
A Formalized General Theory of Syntax with Bindings. CoRR (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58 (1) (2017)
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
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS (2017)
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. IEEE Symposium on Security and Privacy (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017)
Ondrej Kuncar, Andrei Popescu
Comprehending Isabelle/HOL's Consistency. ESOP (2017)
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
Foundational nonuniform (Co)datatypes for higher-order logic. LICS (2017)
Ondrej Kuncar, Andrei Popescu
From Types to Sets by Local Type Definitions in Higher-Order Logic. ITP (2016)
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMed: A Confidentiality-Verified Social Media Platform. ITP (2016)
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. 12 (4) (2016)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational extensible corecursion: a proof assistant perspective. ICFP (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational Extensible Corecursion. CoRR (2015)
Ondrej Kuncar, Andrei Popescu
A Consistent Foundation for Isabelle/HOL. ITP (2015)
Andrei Popescu, Grigore Rosu
Term-generic logic. Theor. Comput. Sci. 577 (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Witnessing (Co)datatypes. ESOP (2015)
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
Truly Modular (Co)datatypes for Isabelle/HOL. ITP (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Cardinals in Isabelle/HOL. ITP (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Abstract Completeness. Arch. Formal Proofs 2014 (2014)
Andrei Popescu, Peter Lammich
Bounded-Deducibility Security. Arch. Formal Proofs 2014 (2014)
Sudeep Kanav, Peter Lammich, Andrei Popescu
A Conference Management System with Verified Document Confidentiality. CAV (2014)
Tobias Nipkow, Andrei Popescu
Making security type systems less ad hoc. it Inf. Technol. 56 (6) (2014)
Markus N. Rabe, Peter Lammich, Andrei Popescu
A shallow embedding of HyperCTL. Arch. Formal Proofs 2014 (2014)
Andrei Popescu, Johannes Hölzl
Probabilistic Noninterference. Arch. Formal Proofs 2014 (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR (2014)
Andrei Popescu
Security Type Systems as Recursive Predicates. CoRR (2013)
Jasmin Christian Blanchette, Andrei Popescu
Mechanizing the Metatheory of Sledgehammer. FroCos (2013)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. 6 (1) (2013)
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding Monomorphic and Polymorphic Types. TACAS (2013)
Andreas Schropp, Andrei Popescu
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. CPP (2013)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formalizing Probabilistic Noninterference. CPP (2013)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO (2013)
Jasmin Christian Blanchette, Andrei Popescu
Sound and Complete Sort Encodings for First-Order Logic. Arch. Formal Proofs 2013 (2013)
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP (2012)
Andrei Popescu, Johannes Hölzl
Possibilistic Noninterference. Arch. Formal Proofs 2012 (2012)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Proving Concurrent Noninterference. CPP (2012)
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS (2012)
Andrei Popescu, Elsa L. Gunter
Recursion principles for syntax with bindings and substitution. ICFP (2011)
Andrei Popescu, Elsa L. Gunter
Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. FoSSaCS (2010)
Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn
Strong Normalization for System F by HOAS on Top of FOAS. LICS (2010)
Andrei Popescu
Weak Bisimilarity Coalgebraically. CALCO (2009)
Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu
A semantic approach to interpolation. Theor. Comput. Sci. 410 (12-13) (2009)
Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu
Theory support for weak higher order abstract syntax in Isabelle/HOL. LFMTP (2009)
Andrei Popescu
Ordinals and Cardinals. Arch. Formal Proofs 2009 (2009)
Andrei Popescu, Grigore Rosu
Term-Generic Logic. WADT (2008)
Daniel Gâinâ, Andrei Popescu
An Institution-Independent Proof of the Robinson Consistency Theorem. Stud Logica 85 (1) (2007)
Daniel Gâinâ, Andrei Popescu
An Institution-independent Generalization of Tarski's Elementary Chain Theorem. J. Log. Comput. 16 (6) (2006)
George Georgescu, Andrei Popescu
A common generalization for MV-algebras and Lukasiewicz-Moisil algebras. Arch. Math. Log. 45 (8) (2006)
George Georgescu, Andrei Popescu
A New Class of Probabilities on Lukasiewicz-Moisil Algebras. J. Multiple Valued Log. Soft Comput. 12 (3-4) (2006)
George Geordesce, Ioana Leustean, Andrei Popescu
Order Convergence and Distance on Lukasiewicz-Moisil Algebras. J. Multiple Valued Log. Soft Comput. 12 (1-2) (2006)
Andrei Popescu, Traian Serbanuta, Grigore Rosu
A Semantic Approach to Interpolation. FoSSaCS (2006)
Andrei Popescu
Lukasiewicz-Moisil Relation Algebras. Stud Logica 81 (2) (2005)
George Georgescu, Andrei Popescu
Similarity Convergence in Residuated Structures. Log. J. IGPL 13 (4) (2005)
Andrei Popescu, Grigore Rosu
Behavioral Extensions of Institutions. CALCO (2005)
George Georgescu, Andrei Popescu
Non-commutative fuzzy structures and pairs of weak negations. Fuzzy Sets Syst. 143 (1) (2004)
Andrei Popescu
A general approach to fuzzy concepts. Math. Log. Q. 50 (3) (2004)
Andrei Popescu
Languages Generated Using an Abstract Catenation. Grammars 7 (2004)
George Georgescu, Andrei Popescu
Non-dual fuzzy connections. Arch. Math. Log. 43 (8) (2004)
George Georgescu, Andrei Popescu
Non-commutative fuzzy Galois connections. Soft Comput. 7 (7) (2003)
George Georgescu, Andrei Popescu
Concept lattices and similarity in non-commutative fuzzy logic. Fundam. Informaticae 53 (1) (2002)