Formal Representation of Mathematics in a Dependently Typed Set Theory. - Feryal Fulya Horozal; Chad E. Brown (Calculemus/MKM, 2007)

A Proof Theoretic Interpretation of Model Theoretic Hiding. - Mihai Codescu; Feryal Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe 001 (WADT, 2010)

Towards Logical Frameworks in the Heterogeneous Tool Set Hets. - Mihai Codescu; Feryal Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe 001; Kristina Sojakova (WADT, 2010)

Project Abstract: Logic Atlas and Integrator (LATIN). - Mihai Codescu; Feryal Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe 001 (Calculemus/MKM, 2011)

Combining Source, Content, Presentation, Narration, and Relational Representation. - Feryal Fulya Horozal; Alin Iacob; Constantin Jucovschi; Michael Kohlhase; Florian Rabe 001 (Calculemus/MKM, 2011)

Representing model theory in a type-theoretical logical framework. - Feryal Fulya Horozal; Florian Rabe 001 (Theor. Comput. Sci., 2011)

Extending MKM Formats at the Statement Level. - Feryal Fulya Horozal; Michael Kohlhase; Florian Rabe 001 (AISC/MKM/Calculemus, 2012)

Compiling Logics. - Mihai Codescu; Feryal Fulya Horozal; Aivaras Jakubauskas; Till Mossakowski; Florian Rabe 001 (WADT, 2012)

Flexary Operators for Formalized Mathematics. - Feryal Fulya Horozal; Florian Rabe 001; Michael Kohlhase (CICM, 2014)

A Framework for Defining Declarative Languages. - Feryal Fulya Horozal (2014)

Formal Logic Definitions for Interchange Languages. - Feryal Fulya Horozal; Florian Rabe 001 (CICM, 2015)