-
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
Bindings As Bounded Natural Functors
To appear in
POPL 2019
-
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMed: A Confidentiality-Verified Social Media Platform (extended version)
Journal of Automated Reasoning 61(1-4): 113-139 (2018)
(Special issue on Milestones in Interactive Thoerem Proving, dedicated to Tobias Nipkow's 60th birthday)
-
Ondřej Kunčar, Andrei Popescu
Safety and conservativity of definitions in HOL and Isabelle/HOL
POPL 2018
Article No. 24, 1-24, ACM
-
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
Foundational nonuniform (co)datatypes for higher-order logic
LICS 2017
1-12, ACM / IEEE
-
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMeDis: A Distributed Social Media Platform
with Formally Verified Confidentiality Guarantees
Security and Privacy 2017
729-748, IEEE
-
Ondřej Kunčar, Andrei Popescu
Comprehending Isabelle/HOL's consistency
ESOP 2017
LNCS 10201, 724-749, Springer
-
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel
Friends with benefits: Implementing corecursion in foundational proof assistants
ESOP 2017
LNCS 10201, 111-140, Springer
Here are the
slides
for my two end-to-end ESOP 2017 talks.
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Soundness and completeness proofs by coinductive methods
Journal of Automated Reasoning 58(1): 149-179 (2017)
(Special issue dedicated to
IJCAR 2014)
-
Lorenzo Gheri, Andrei Popescu
A Formalized General Theory of Syntax With Bindings
ITP 2017
LNCS 10499, 241-261, Springer
-
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding monomorphic and polymorphic types
Logical Methods in Computer Science 12(4), 2016
(Special issue dedicated to TACAS 2013)
-
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMed: A Confidentiality-Verified Social Media Platform
ITP 2016
LNCS 9807, 87-106, Springer
-
Ondřej Kunčar, Andrei Popescu
From Types to Sets by Local Type Definitions in Higher-Order Logic
ITP 2016
LNCS 9807, 200-218, Springer
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational Extensible Corecursion: A Proof Assistant Perspective
ICFP 2015
192-204, ACM
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Witnessing (Co)datatypes
ESOP 2015
LNCS 9032, 359-382, Springer
-
Andrei Popescu, Grigore Roșu
Term-Generic Logic
Theoretical Computer Science 577: 1–24 (2015)
-
Ondřej Kunčar, Andrei Popescu
A Consistent Foundation for Isabelle/HOL
ITP 2015
LNCS 9236, 234-252, Springer
-
Sudeep Kanav, Peter Lammich, Andrei Popescu
A Conference Management System with Verified Document Confidentiality
CAV 2014
LNCS 8559, 167-183, Springer
-
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
Truly Modular (Co)datatypes for Isabelle/HOL
ITP 2014
LNCS 8558, 93-110, Springer
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Cardinals in Isabelle/HOL
ITP 2014
LNCS 8558, 111-127, Springer
-
Tobias Nipkow, Andrei Popescu
Making Security Type Systems Less Ad Hoc
it - Information Technology 56(6): 267-272 (2014)
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Unified Classical Logic Completeness: A Coinductive Pearl
IJCAR 2014
LNCS 8562, 46-60, Springer
-
Ondřej Kunčar, Andrei Popescu
From Types to Sets in Isabelle/HOL
Isabelle Workshop 2014
-
Andreas Schropp, Andrei Popescu
Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory
CPP 2013
LNCS 8307, 114-130, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formalizing Probabilistic Noninterference
CPP 2013
LNCS 8307, 259-275, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formal Verification of Language-Based Concurrent Noninterference
Journal of Formalized Reasoning 6(1), 2013
-
Jasmin Christian Blanchette, Andrei Popescu
Mechanizing the metatheory of Sledgehammer
FroCoS 2013
LNCS 8152, 245-260, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Noninterfering Schedulers: When Possibilistic Noninterference Implies Probabilistic Noninterference
CALCO 2013
LNCS 8089, 236-252, Springer
-
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding Monomorphic and Polymorphic Types
TACAS 2013
LNCS 7795, 493-507, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Proving Concurrent Noninterference
CPP 2012
LNCS 7795, 109-125, Springer
Proud receiver of the
RS3
best paper award for 2012-2013
-
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification
ITP 2012
LNCS 7406, 345-360, Springer
-
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, IEEE
-
Andrei Popescu, Elsa L. Gunter
Recursion principles for syntax with bindings and substitution
ICFP 2011
346-358, ACM
-
Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn
Strong Normalization for System F by HOAS on Top of FOAS
LICS 2010
31-40, IEEE
-
Andrei Popescu, Elsa L. Gunter
Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
FOSSACS 2010
LNCS 6014, 109-127, Springer
-
Andrei Popescu, Traian Florin Șerbănuță, Grigore Roșu
A semantic approach to interpolation
Theoretical Computer Science 410(12-13): 1109-1128 (2009)
-
Andrei Popescu
Weak Bisimilarity Coalgebraically
CALCO 2009
LNCS 5728, 157-172, Springer
-
Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu
Theory support for weak higher order abstract syntax in Isabelle/HOL
LFMTP 2009
12-20, ACM
-
Andrei Popescu, Grigore Roșu
Term-Generic Logic.
WADT 2008
LNCS 5486, 290-307, Springer
-
Daniel Găină, Andrei Popescu
An Institution-Independent Proof of the Robinson Consistency Theorem
Studia Logica 85(1): 41-73 (2007)
-
Daniel Găină, Andrei Popescu
An Institution-independent Generalization of Tarski's Elementary Chain Theorem
Journal of Logic and Computation 16(6): 713-735 (2006)
-
Andrei Popescu, Traian Florin Șerbănuță, Grigore Roșu
A Semantic Approach to Interpolation
FOSSACS 2006
LNCS 3921, 307-321, Springer
-
Andrei Popescu, Grigore Roșu
Behavioral Extensions of Institutions
CALCO 2005
LNCS 3629, 331-347, Springer
-
Andrei Popescu
Languages Generated Using an Abstract Catenation
Grammars 7: 31-40 (2004)