Collaborated with:O.Kuncar D.Traytel J.C.Blanchette Lorenzo Gheri A.Bouzy A.Lochbihler
Talks about:hol (3) isabell (2) comprehend (1) incomplet (1) implement (1) corecurs (1) abstract (1) theorem (1) functor (1) foundat (1)
Person: Andrei Popescu 0001
DBLP: 0001:Andrei_Popescu
Contributed to:
2017
2019
20182019Wrote 5 papers:
- ESOP-2017-BlanchetteBL0T #implementation #proving #recursion
- Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants (JCB, AB, AL, AP0, DT), pp. 111–140.
- ESOP-2017-Kuncar0 #consistency #higher-order
- Comprehending Isabelle/HOL's Consistency (OK, AP0), pp. 724–749.
- CADE-2019-0001T #theorem
- A Formally Verified Abstract Account of Gödel's Incompleteness Theorems (AP0, DT), pp. 442–461.
- POPL-2018-Kuncar0 #higher-order #safety
- Safety and conservativity of definitions in HOL and Isabelle/HOL (OK, AP0), p. 26.
- POPL-2019-BlanchetteGPT #bound
- Bindings as bounded natural functors (JCB, LG, AP0, DT), p. 34.