Andrei Popescu

Orcid: 0000-0001-8747-0619

Affiliations:
  • University of Sheffield, Department of Computer Science, UK
  • Middlesex University London, School of Science and Technology, UK (former)
  • TU Munich, Faculty of Computer Science, Germany (former)
  • University of Illinois at Urbana-Champaign, Department of Computer Science, IL, USA (former)
  • University of Bucharest, Faculty of Mathematics, Romania (former)


According to our database1, Andrei Popescu authored at least 87 papers between 2002 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Nominal Recursors as Epi-Recursors.
Proc. ACM Program. Lang., January, 2024

The Complex(ity) Landscape of Checking Infinite Descent.
Proc. ACM Program. Lang., January, 2024

2023
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version.
J. Autom. Reason., September, 2023

Admissible Types-to-PERs Relativization in Higher-Order Logic.
Proc. ACM Program. Lang., January, 2023

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

A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress).
Proceedings of the iFM 2023 - 18th International Conference, 2023

2022
Rensets and Renaming-Based Recursion for Syntax with Bindings.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
CoCon: A Conference Management System with Formally Verified Document Confidentiality.
J. Autom. Reason., 2021

Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant.
J. Autom. Reason., 2021

Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS.
CoRR, 2021

CoCon: A Confidentiality-Verified Conference Management System.
Arch. Formal Proofs, 2021

Fresh identifiers.
Arch. Formal Proofs, 2021

CoSMed: A confidentiality-verified social media platform.
Arch. Formal Proofs, 2021

CoSMeDis: A confidentiality-verified distributed social media platform.
Arch. Formal Proofs, 2021

Compositional BD Security.
Arch. Formal Proofs, 2021

Bounded-Deducibility Security (Invited Paper).
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020
A Formalized General Theory of Syntax with Bindings: Extended Version.
J. Autom. Reason., 2020

Syntax-Independent Logic Infrastructure.
Arch. Formal Proofs, 2020

Robinson Arithmetic.
Arch. Formal Proofs, 2020

An Abstract Formalization of Gödel's Incompleteness Theorems.
Arch. Formal Proofs, 2020

From Abstract to Concrete Gödel's Incompleteness Theorems - Part II.
Arch. Formal Proofs, 2020

From Abstract to Concrete Gödel's Incompleteness Theorems - Part I.
Arch. Formal Proofs, 2020

2019
Bindings as bounded natural functors.
Proc. ACM Program. Lang., 2019

A Consistent Foundation for Isabelle/HOL.
J. Autom. Reason., 2019

From Types to Sets by Local Type Definition in Higher-Order Logic.
J. Autom. Reason., 2019

A General Theory of Syntax with Bindings.
Arch. Formal Proofs, 2019

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
Safety and conservativity of definitions in HOL and Isabelle/HOL.
Proc. ACM Program. Lang., 2018

CoSMed: A Confidentiality-Verified Social Media Platform.
J. Autom. Reason., 2018

Introduction to Milestones in Interactive Theorem Proving.
J. Autom. Reason., 2018

2017
Soundness and Completeness Proofs by Coinductive Methods.
J. Autom. Reason., 2017

Operations on Bounded Natural Functors.
Arch. Formal Proofs, 2017

Abstract Soundness.
Arch. Formal Proofs, 2017

CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees.
Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

Foundational nonuniform (Co)datatypes for higher-order logic.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

A Formalized General Theory of Syntax with Bindings.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Comprehending Isabelle/HOL's Consistency.
Proceedings of the Programming Languages and Systems, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.
Proceedings of the Programming Languages and Systems, 2017

2016
Encoding Monomorphic and Polymorphic Types.
Log. Methods Comput. Sci., 2016

From Types to Sets by Local Type Definitions in Higher-Order Logic.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015
Term-generic logic.
Theor. Comput. Sci., 2015

Foundational Extensible Corecursion.
CoRR, 2015

Foundational extensible corecursion: a proof assistant perspective.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Witnessing (Co)datatypes.
Proceedings of the Programming Languages and Systems, 2015

2014
Making security type systems less ad hoc.
it Inf. Technol., 2014

A shallow embedding of HyperCTL.
Arch. Formal Proofs, 2014

Bounded-Deducibility Security.
Arch. Formal Proofs, 2014

Abstract Completeness.
Arch. Formal Proofs, 2014

Probabilistic Noninterference.
Arch. Formal Proofs, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Cardinals in Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

A Conference Management System with Verified Document Confidentiality.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Unified Classical Logic Completeness - A Coinductive Pearl.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
Formal Verification of Language-Based Concurrent Noninterference.
J. Formaliz. Reason., 2013

Security Type Systems as Recursive Predicates.
CoRR, 2013

Sound and Complete Sort Encodings for First-Order Logic.
Arch. Formal Proofs, 2013

Mechanizing the Metatheory of Sledgehammer.
Proceedings of the Frontiers of Combining Systems, 2013

Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Formalizing Probabilistic Noninterference.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference.
Proceedings of the Algebra and Coalgebra in Computer Science, 2013

2012
Possibilistic Noninterference.
Arch. Formal Proofs, 2012

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Proving Concurrent Noninterference.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Recursion principles for syntax with bindings and substitution.
Proceedings of the Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011

2010
Contributions to the theory of syntax with bindings and to process algebra
PhD thesis, 2010

Strong Normalization for System F by HOAS on Top of FOAS.
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization.
Proceedings of the Foundations of Software Science and Computational Structures, 2010

2009
A semantic approach to interpolation.
Theor. Comput. Sci., 2009

Ordinals and Cardinals.
Arch. Formal Proofs, 2009

Theory support for weak higher order abstract syntax in Isabelle/HOL.
Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009

Weak Bisimilarity Coalgebraically.
Proceedings of the Algebra and Coalgebra in Computer Science, 2009

2007
An Institution-Independent Proof of the Robinson Consistency Theorem.
Stud Logica, 2007

2006
A New Class of Probabilities on Lukasiewicz-Moisil Algebras.
J. Multiple Valued Log. Soft Comput., 2006

Order Convergence and Distance on Lukasiewicz-Moisil Algebras.
J. Multiple Valued Log. Soft Comput., 2006

An Institution-independent Generalization of Tarski's Elementary Chain Theorem.
J. Log. Comput., 2006

A common generalization for MV-algebras and Lukasiewicz-Moisil algebras.
Arch. Math. Log., 2006

2005
Lukasiewicz-Moisil Relation Algebras.
Stud Logica, 2005

Similarity Convergence in Residuated Structures.
Log. J. IGPL, 2005

Behavioral Extensions of Institutions.
Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

2004
A general approach to fuzzy concepts.
Math. Log. Q., 2004

Languages Generated Using an Abstract Catenation.
Grammars, 2004

Non-commutative fuzzy structures and pairs of weak negations.
Fuzzy Sets Syst., 2004

Non-dual fuzzy connections.
Arch. Math. Log., 2004

2003
Non-commutative fuzzy Galois connections.
Soft Comput., 2003

2002
Concept lattices and similarity in non-commutative fuzzy logic.
Fundam. Informaticae, 2002


  Loading...