System Description: The Proof Transformation System CERES. - Tsvetan Dunchev; Alexander Leitsch; Tomer Libal; Daniel Weller 001; Bruno Woltzenlogel Paleo (IJCAR, 2010)

System Feature Description: Importing Refutations into the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (PxTP, 2012)

PROOFTOOL: a GUI for the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (UITP, 2012)

Cut-Elimination and Proof Schemata. - Cvetan Dunchev; Alexander Leitsch; Mikheil Rukhaia; Daniel Weller 001 (TbiLLC, 2013)

CERES for First-Order Schemata - Cvetan Dunchev; Alexander Leitsch; Mikheil Rukhaia; Daniel Weller 001 (CoRR, 2013)

ELPI: Fast, Embeddable, λProlog Interpreter. - Cvetan Dunchev; Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi (LPAR, 2015)

Formalizing Physics: Automation, Presentation and Foundation Issues. - Cezary Kaliszyk; Josef Urban; Umair Siddique; Sanaz Khan Afshar; Cvetan Dunchev; Sofiène Tahar (CICM, 2015)

Enabling Symbolic and Numerical Computations in HOL Light. - Ons Seddiki; Cvetan Dunchev; Sanaz Khan Afshar; Sofiène Tahar (CICM, 2015)

Implementing HOL in an Higher Order Logic Programming Language. - Cvetan Dunchev; Claudio Sacerdoti Coen; Enrico Tassi (LFMTP, 2016)

Formal Analysis of Information Flow in HOL. - Ghassen Helali; Sofiène Tahar; Osman Hasan; Tsvetan Dunchev (SETTA, 2017)