Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndrei Popescu 0001
Person information
- affiliation: University of Sheffield, Department of Computer Science, UK
- affiliation (former): Middlesex University London, School of Science and Technology, UK
- affiliation (former): TU Munich, Faculty of Computer Science, Germany
- affiliation (former): University of Illinois at Urbana-Champaign, Department of Computer Science, IL, USA
- affiliation (former): University of Bucharest, Faculty of Mathematics, Romania
Other persons with the same name
- Andrei Popescu — disambiguation page
- Andrei Popescu 0002
![[0000-0002-0906-5527]](https://dblp.uni-trier.de/img/orcid-mark.12x12.png "0000-0002-0906-5527")
— University Grenoble Alpes, CNRS, Grenoble INP, Institute of Engineering, France - Andrei Popescu 0003 — Nokia Research Center, Helsinki
- Andrei Popescu 0004 — ENST Télécom ParisTech
- Andrei Popescu 0005 — Ghent University, Belgium (and 3 more)
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Books and Theses
- 2010
[b1]Andrei Popescu:
Contributions to the theory of syntax with bindings and to process algebra. University of Illinois Urbana-Champaign, USA, 2010
Journal Articles
- 2024
- [j53]Andrei Popescu:
Nominal Recursors as Epi-Recursors. Proc. ACM Program. Lang. 8(POPL): 425-456 (2024) - [j52]Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe:
The Complex(ity) Landscape of Checking Infinite Descent. Proc. ACM Program. Lang. 8(POPL): 1352-1384 (2024) - 2023
- [j51]Andrei Popescu:
Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion. Arch. Formal Proofs 2023 (2023) - [j50]Andrei Popescu:
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version. J. Autom. Reason. 67(3): 23 (2023) - [j49]Andrei Popescu, Dmitriy Traytel:
Admissible Types-to-PERs Relativization in Higher-Order Logic. Proc. ACM Program. Lang. 7(POPL): 1214-1245 (2023) - 2021
- [j48]Thomas Bauereiss, Andrei Popescu:
Compositional BD Security. Arch. Formal Proofs 2021 (2021) - [j47]Thomas Bauereiss, Andrei Popescu:
CoSMeDis: A confidentiality-verified distributed social media platform. Arch. Formal Proofs 2021 (2021) - [j46]Thomas Bauereiss, Andrei Popescu:
CoSMed: A confidentiality-verified social media platform. Arch. Formal Proofs 2021 (2021) - [j45]Andrei Popescu, Thomas Bauereiss:
Fresh identifiers. Arch. Formal Proofs 2021 (2021) - [j44]Andrei Popescu, Peter Lammich, Thomas Bauereiss:
CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs 2021 (2021) - [j43]Andrei Popescu, Peter Lammich, Ping Hou:
CoCon: A Conference Management System with Formally Verified Document Confidentiality. J. Autom. Reason. 65(2): 321-356 (2021) - [j42]Andrei Popescu, Dmitriy Traytel:
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. J. Autom. Reason. 65(7): 1027-1070 (2021) - 2020
- [j41]Andrei Popescu, Dmitriy Traytel:
From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. Arch. Formal Proofs 2020 (2020) - [j40]Andrei Popescu, Dmitriy Traytel:
From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. Arch. Formal Proofs 2020 (2020) - [j39]Andrei Popescu, Dmitriy Traytel:
An Abstract Formalization of Gödel's Incompleteness Theorems. Arch. Formal Proofs 2020 (2020) - [j38]Andrei Popescu, Dmitriy Traytel:
Robinson Arithmetic. Arch. Formal Proofs 2020 (2020) - [j37]Andrei Popescu, Dmitriy Traytel:
Syntax-Independent Logic Infrastructure. Arch. Formal Proofs 2020 (2020) - [j36]Lorenzo Gheri, Andrei Popescu:
A Formalized General Theory of Syntax with Bindings: Extended Version. J. Autom. Reason. 64(4): 641-675 (2020) - 2019
- [j35]Lorenzo Gheri, Andrei Popescu:
A General Theory of Syntax with Bindings. Arch. Formal Proofs 2019 (2019) - [j34]Ondrej Kuncar, Andrei Popescu:
From Types to Sets by Local Type Definition in Higher-Order Logic. J. Autom. Reason. 62(2): 237-260 (2019) - [j33]Ondrej Kuncar, Andrei Popescu:
A Consistent Foundation for Isabelle/HOL. J. Autom. Reason. 62(4): 531-555 (2019) - [j32]Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel:
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3(POPL): 22:1-22:34 (2019) - 2018
- [j31]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): 1-8 (2018) - [j30]Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi:
CoSMed: A Confidentiality-Verified Social Media Platform. J. Autom. Reason. 61(1-4): 113-139 (2018) - [j29]Ondrej Kuncar, Andrei Popescu:
Safety and conservativity of definitions in HOL and Isabelle/HOL. Proc. ACM Program. Lang. 2(POPL): 24:1-24:26 (2018) - 2017
- [j28]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Soundness. Arch. Formal Proofs 2017 (2017) - [j27]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017) - [j26]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58(1): 149-179 (2017) - 2016
- [j25]Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. 12(4) (2016) - 2015
- [j24]Andrei Popescu, Grigore Rosu:
Term-generic logic. Theor. Comput. Sci. 577: 1-24 (2015) - 2014
- [j23]Andrei Popescu, Johannes Hölzl:
Probabilistic Noninterference. Arch. Formal Proofs 2014 (2014) - [j22]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Completeness. Arch. Formal Proofs 2014 (2014) - [j21]Andrei Popescu, Peter Lammich:
Bounded-Deducibility Security. Arch. Formal Proofs 2014 (2014) - [j20]Markus N. Rabe, Peter Lammich, Andrei Popescu:
A shallow embedding of HyperCTL. Arch. Formal Proofs 2014 (2014) - [j19]Tobias Nipkow, Andrei Popescu:
Making security type systems less ad hoc. it Inf. Technol. 56(6): 267-272 (2014) - 2013
- [j18]Jasmin Christian Blanchette, Andrei Popescu:
Sound and Complete Sort Encodings for First-Order Logic. Arch. Formal Proofs 2013 (2013) - [j17]Andrei Popescu, Johannes Hölzl, Tobias Nipkow:
Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. 6(1): 1-30 (2013) - 2012
- [j16]Andrei Popescu, Johannes Hölzl:
Possibilistic Noninterference. Arch. Formal Proofs 2012 (2012) - 2009
- [j15]Andrei Popescu:
Ordinals and Cardinals. Arch. Formal Proofs 2009 (2009) - [j14]Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu:
A semantic approach to interpolation. Theor. Comput. Sci. 410(12-13): 1109-1128 (2009) - 2007
- [j13]Daniel Gâinâ, Andrei Popescu:
An Institution-Independent Proof of the Robinson Consistency Theorem. Stud Logica 85(1): 41-73 (2007) - 2006
- [j12]George Georgescu, Andrei Popescu:
A common generalization for MV-algebras and Lukasiewicz-Moisil algebras. Arch. Math. Log. 45(8): 947-981 (2006) - [j11]Daniel Gâinâ, Andrei Popescu:
An Institution-independent Generalization of Tarski's Elementary Chain Theorem. J. Log. Comput. 16(6): 713-735 (2006) - [j10]George Geordesce, Ioana Leustean, Andrei Popescu:
Order Convergence and Distance on Lukasiewicz-Moisil Algebras. J. Multiple Valued Log. Soft Comput. 12(1-2): 33-39 (2006) - [j9]George Georgescu, Andrei Popescu:
A New Class of Probabilities on Lukasiewicz-Moisil Algebras. J. Multiple Valued Log. Soft Comput. 12(3-4): 337-354 (2006) - 2005
- [j8]George Georgescu, Andrei Popescu:
Similarity Convergence in Residuated Structures. Log. J. IGPL 13(4): 389-413 (2005) - [j7]Andrei Popescu:
Lukasiewicz-Moisil Relation Algebras. Stud Logica 81(2): 167-189 (2005) - 2004
- [j6]George Georgescu, Andrei Popescu:
Non-dual fuzzy connections. Arch. Math. Log. 43(8): 1009-1039 (2004) - [j5]George Georgescu, Andrei Popescu:
Non-commutative fuzzy structures and pairs of weak negations. Fuzzy Sets Syst. 143(1): 129-155 (2004) - [j4]Andrei Popescu:
Languages Generated Using an Abstract Catenation. Grammars 7: 31-40 (2004) - [j3]Andrei Popescu:
A general approach to fuzzy concepts. Math. Log. Q. 50(3): 265-280 (2004) - 2003
- [j2]George Georgescu, Andrei Popescu:
Non-commutative fuzzy Galois connections. Soft Comput. 7(7): 458-467 (2003) - 2002
- [j1]George Georgescu, Andrei Popescu:
Concept lattices and similarity in non-commutative fuzzy logic. Fundam. Informaticae 53(1): 23-54 (2002)
Conference and Workshop Papers
- 2023
- [c35]Artur Graczyk, Marialena Hadjikosti, Andrei Popescu:
A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress). iFM 2023: 391-397 - 2022
- [c34]Andrei Popescu:
Rensets and Renaming-Based Recursion for Syntax with Bindings. IJCAR 2022: 618-639 - 2021
- [c33]Andrei Popescu, Thomas Bauereiss, Peter Lammich:
Bounded-Deducibility Security (Invited Paper). ITP 2021: 3:1-3:20 - 2019
- [c32]Andrei Popescu, Dmitriy Traytel:
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. CADE 2019: 442-461 - 2017
- [c31]Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel:
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP 2017: 111-140 - [c30]Ondrej Kuncar, Andrei Popescu:
Comprehending Isabelle/HOL's Consistency. ESOP 2017: 724-749 - [c29]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: 3-21 - [c28]Lorenzo Gheri, Andrei Popescu:
A Formalized General Theory of Syntax with Bindings. ITP 2017: 241-261 - [c27]Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel:
Foundational nonuniform (Co)datatypes for higher-order logic. LICS 2017: 1-12 - [c26]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: 729-748 - 2016
- [c25]Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi:
CoSMed: A Confidentiality-Verified Social Media Platform. ITP 2016: 87-106 - [c24]Ondrej Kuncar, Andrei Popescu:
From Types to Sets by Local Type Definitions in Higher-Order Logic. ITP 2016: 200-218 - 2015
- [c23]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Witnessing (Co)datatypes. ESOP 2015: 359-382 - [c22]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational extensible corecursion: a proof assistant perspective. ICFP 2015: 192-204 - [c21]Ondrej Kuncar, Andrei Popescu:
A Consistent Foundation for Isabelle/HOL. ITP 2015: 234-252 - 2014
- [c20]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR 2014: 46-60 - [c19]Sudeep Kanav, Peter Lammich, Andrei Popescu:
A Conference Management System with Verified Document Confidentiality. CAV 2014: 167-183 - [c18]Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel:
Truly Modular (Co)datatypes for Isabelle/HOL. ITP 2014: 93-110 - [c17]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Cardinals in Isabelle/HOL. ITP 2014: 111-127 - 2013
- [c16]Andrei Popescu, Johannes Hölzl, Tobias Nipkow:
Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO 2013: 236-252 - [c15]Andreas Schropp, Andrei Popescu:
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. CPP 2013: 114-130 - [c14]Andrei Popescu, Johannes Hölzl, Tobias Nipkow:
Formalizing Probabilistic Noninterference. CPP 2013: 259-275 - [c13]Jasmin Christian Blanchette, Andrei Popescu:
Mechanizing the Metatheory of Sledgehammer. FroCos 2013: 245-260 - [c12]Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. TACAS 2013: 493-507 - 2012
- [c11]Andrei Popescu, Johannes Hölzl, Tobias Nipkow:
Proving Concurrent Noninterference. CPP 2012: 109-125 - [c10]Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach:
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP 2012: 345-360 - [c9]Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette:
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS 2012: 596-605 - 2011
- [c8]Andrei Popescu, Elsa L. Gunter:
Recursion principles for syntax with bindings and substitution. ICFP 2011: 346-358 - 2010
- [c7]Andrei Popescu, Elsa L. Gunter:
Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. FoSSaCS 2010: 109-127 - [c6]Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn:
Strong Normalization for System F by HOAS on Top of FOAS. LICS 2010: 31-40 - 2009
- [c5]Andrei Popescu:
Weak Bisimilarity Coalgebraically. CALCO 2009: 157-172 - [c4]Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu:
Theory support for weak higher order abstract syntax in Isabelle/HOL. LFMTP 2009: 12-20 - 2008
- [c3]Andrei Popescu, Grigore Rosu:
Term-Generic Logic. WADT 2008: 290-307 - 2006
- [c2]Andrei Popescu, Traian Serbanuta, Grigore Rosu:
A Semantic Approach to Interpolation. FoSSaCS 2006: 307-321 - 2005
- [c1]Andrei Popescu, Grigore Rosu:
Behavioral Extensions of Institutions. CALCO 2005: 331-347
Editorship
- 2022
- [e4]Andrei Popescu, Steve Zdancewic:
CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. ACM 2022, ISBN 978-1-4503-9182-5 [contents] - 2021
- [e3]Catalin Hritcu, Andrei Popescu:
CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021. ACM 2021, ISBN 978-1-4503-8299-1 [contents] - 2019
- [e2]Andreas Herzig, Andrei Popescu:
Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings. Lecture Notes in Computer Science 11715, Springer 2019, ISBN 978-3-030-29006-1 [contents] - [e1]Serenella Cerrito, Andrei Popescu:
Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings. Lecture Notes in Computer Science 11714, Springer 2019, ISBN 978-3-030-29025-2 [contents]
Informal and Other Publications
- 2023
- [i6]Andrei Popescu:
Nominal Recursors as Epi-Recursors. CoRR abs/2301.00894 (2023) - 2022
- [i5]Andrei Popescu:
Rensets and Renaming-Based Recursion for Syntax with Bindings. CoRR abs/2205.09233 (2022) - 2021
- [i4]Lorenzo Gheri, Andrei Popescu:
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS. CoRR abs/2107.11674 (2021) - 2017
- [i3]Lorenzo Gheri, Andrei Popescu:
A Formalized General Theory of Syntax with Bindings. CoRR abs/1707.00024 (2017) - 2015
- [i2]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational Extensible Corecursion. CoRR abs/1501.05425 (2015) - 2013
- [i1]Andrei Popescu:
Security Type Systems as Recursive Predicates. CoRR abs/1308.3472 (2013)
Coauthor Index
Jasmin Blanchette
aka: Jasmin Christian Blanchette
aka: Jasmin Christian Blanchette
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-13 21:46 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
