Andrei Popescu

Proc. ACM Program. Lang., January, 2024

The Complex(ity) Landscape of Checking Infinite Descent.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., January, 2024

2023

Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version.

[BibT_eX]

[DOI]

J. Autom. Reason., September, 2023

Admissible Types-to-PERs Relativization in Higher-Order Logic.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., January, 2023

Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2023

A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress).

[BibT_eX]

[DOI]

Artur Graczyk

Marialena Hadjikosti

Proceedings of the iFM 2023 - 18th International Conference, 2023

2022

Rensets and Renaming-Based Recursion for Syntax with Bindings.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

CoCon: A Conference Management System with Formally Verified Document Confidentiality.

[BibT_eX]

[DOI]

Ping Hou

J. Autom. Reason., 2021

Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

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

[BibT_eX]

[DOI]

CoRR, 2021

CoCon: A Confidentiality-Verified Conference Management System.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Fresh identifiers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

CoSMed: A confidentiality-verified social media platform.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

CoSMeDis: A confidentiality-verified distributed social media platform.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Compositional BD Security.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Bounded-Deducibility Security (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

A Formalized General Theory of Syntax with Bindings: Extended Version.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Syntax-Independent Logic Infrastructure.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Robinson Arithmetic.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

An Abstract Formalization of Gödel's Incompleteness Theorems.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

From Abstract to Concrete Gödel's Incompleteness Theorems - Part II.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

From Abstract to Concrete Gödel's Incompleteness Theorems - Part I.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

2019

Bindings as bounded natural functors.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

A Consistent Foundation for Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

From Types to Sets by Local Type Definition in Higher-Order Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

A General Theory of Syntax with Bindings.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Safety and conservativity of definitions in HOL and Isabelle/HOL.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

CoSMed: A Confidentiality-Verified Social Media Platform.

[BibT_eX]

[DOI]

Thomas Bauereiß

Armando Pesenti Gritti

Franco Raimondi

J. Autom. Reason., 2018

Introduction to Milestones in Interactive Theorem Proving.

[BibT_eX]

[DOI]

Jeremy Avigad

J. Autom. Reason., 2018

2017

Soundness and Completeness Proofs by Coinductive Methods.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Operations on Bounded Natural Functors.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Abstract Soundness.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees.

[BibT_eX]

[DOI]

Thomas Bauereiß

Armando Pesenti Gritti

Franco Raimondi

Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

Foundational nonuniform (Co)datatypes for higher-order logic.

[BibT_eX]

[DOI]

Fabian Meier

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

A Formalized General Theory of Syntax with Bindings.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.

[BibT_eX]

[DOI]

Julian Biendarra

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Comprehending Isabelle/HOL's Consistency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

2016

Encoding Monomorphic and Polymorphic Types.

[BibT_eX]

[DOI]

Sascha Böhme

Nicholas Smallbone

Log. Methods Comput. Sci., 2016

From Types to Sets by Local Type Definitions in Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015

Term-generic logic.

[BibT_eX]

[DOI]

Grigore Rosu

Theor. Comput. Sci., 2015

Foundational Extensible Corecursion.

[BibT_eX]

[DOI]

CoRR, 2015

Foundational extensible corecursion: a proof assistant perspective.

[BibT_eX]

[DOI]

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Witnessing (Co)datatypes.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

2014

Making security type systems less ad hoc.

[BibT_eX]

[DOI]

it Inf. Technol., 2014

A shallow embedding of HyperCTL.

[BibT_eX]

[DOI]

Markus N. Rabe

Arch. Formal Proofs, 2014

Bounded-Deducibility Security.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Abstract Completeness.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Probabilistic Noninterference.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Cardinals in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

A Conference Management System with Verified Document Confidentiality.

[BibT_eX]

[DOI]

Sudeep Kanav

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Unified Classical Logic Completeness - A Coinductive Pearl.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Formal Verification of Language-Based Concurrent Noninterference.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2013

Security Type Systems as Recursive Predicates.

[BibT_eX]

[DOI]

CoRR, 2013

Sound and Complete Sort Encodings for First-Order Logic.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2013

Mechanizing the Metatheory of Sledgehammer.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory.

[BibT_eX]

[DOI]

Andreas Schropp

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Formalizing Probabilistic Noninterference.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2013

2012

Possibilistic Noninterference.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.

[BibT_eX]

[DOI]

Daniel Wand

Christoph Weidenbach

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Proving Concurrent Noninterference.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Recursion principles for syntax with bindings and substitution.

[BibT_eX]

[DOI]

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

[BibT_eX]

[DOI]

PhD thesis, 2010

Strong Normalization for System F by HOAS on Top of FOAS.

[BibT_eX]

[DOI]

Christopher J. Osborn

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2010

2009

A semantic approach to interpolation.

[BibT_eX]

[DOI]

Traian-Florin Serbanuta

Grigore Rosu

Theor. Comput. Sci., 2009

Ordinals and Cardinals.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2009

Theory support for weak higher order abstract syntax in Isabelle/HOL.

[BibT_eX]

[DOI]

Christopher J. Osborn

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009

Weak Bisimilarity Coalgebraically.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2009

2007

An Institution-Independent Proof of the Robinson Consistency Theorem.

[BibT_eX]

[DOI]

Daniel Gâinâ

Stud Logica, 2007

2006

A New Class of Probabilities on Lukasiewicz-Moisil Algebras.

[BibT_eX]

[DOI]

J. Multiple Valued Log. Soft Comput., 2006

Order Convergence and Distance on Lukasiewicz-Moisil Algebras.

[BibT_eX]

[DOI]

George Geordesce

Ioana Leustean

J. Multiple Valued Log. Soft Comput., 2006

An Institution-independent Generalization of Tarski's Elementary Chain Theorem.

[BibT_eX]

[DOI]

Daniel Gâinâ

J. Log. Comput., 2006

A common generalization for MV-algebras and Lukasiewicz-Moisil algebras.

[BibT_eX]

[DOI]

Arch. Math. Log., 2006

2005

Lukasiewicz-Moisil Relation Algebras.

[BibT_eX]

[DOI]

Stud Logica, 2005

Similarity Convergence in Residuated Structures.

[BibT_eX]

[DOI]

Log. J. IGPL, 2005

Behavioral Extensions of Institutions.

[BibT_eX]

[DOI]

Grigore Rosu

Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

2004

A general approach to fuzzy concepts.

[BibT_eX]

[DOI]

Math. Log. Q., 2004

Languages Generated Using an Abstract Catenation.

[BibT_eX]

[DOI]

Grammars, 2004

Non-commutative fuzzy structures and pairs of weak negations.

[BibT_eX]

[DOI]

Fuzzy Sets Syst., 2004

Non-dual fuzzy connections.

[BibT_eX]

[DOI]

Arch. Math. Log., 2004

2003

Non-commutative fuzzy Galois connections.

[BibT_eX]

[DOI]

Soft Comput., 2003

2002

Concept lattices and similarity in non-commutative fuzzy logic.

[BibT_eX]

[DOI]