A Compendium of Continuous Lattices in MIZAR. - Grzegorz Bancerek; Piotr Rudnicki (J. Autom. Reason., 2002)

Information Retrieval in MML. - Grzegorz Bancerek; Piotr Rudnicki (MKM, 2003)

On the structure of Mizar types. - Grzegorz Bancerek (Mathematics, Logic and Computation @ ICALP, 2003)

Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles. - Grzegorz Bancerek; Josef Urban (MKM, 2004)

Information Retrieval and Rendering with. - Grzegorz Bancerek (MKM, 2006)

Presenting and Explaining Mizar. - Josef Urban; Grzegorz Bancerek (UITP@FLoC, 2006)

Mizar Analysis of Algorithms: Algorithms over Integers. - Grzegorz Bancerek (Formaliz. Math., 2008)

Towards the Construction of a Model of Mizar Concepts. - Grzegorz Bancerek (Formaliz. Math., 2008)

Introduction to Matroids. - Grzegorz Bancerek; Yasunari Shidama (Formaliz. Math., 2008)

Epsilon Numbers and Cantor Normal Form. - Grzegorz Bancerek (Formaliz. Math., 2009)

A Model of Mizar Concepts - Unification. - Grzegorz Bancerek (Formaliz. Math., 2010)

Veblen Hierarchy. - Grzegorz Bancerek (Formaliz. Math., 2011)

Sorting by Exchanging. - Grzegorz Bancerek (Formaliz. Math., 2011)

Representation Theorem for Stacks. - Grzegorz Bancerek (Formaliz. Math., 2011)

Semantics of MML Query. - Grzegorz Bancerek (Formaliz. Math., 2012)

Free Term Algebras. - Grzegorz Bancerek (Formaliz. Math., 2012)

Program Algebra over an Algebra. - Grzegorz Bancerek (Formaliz. Math., 2012)

Valuation Theory. Part I. - Grzegorz Bancerek; Hidetsune Kobayashi; Artur Kornilowicz (Formaliz. Math., 2012)

Analysis of Algorithms: An Example of a Sort Algorithm. - Grzegorz Bancerek (Formaliz. Math., 2013)

Semantics of MML Query - Ordering. - Grzegorz Bancerek (Formaliz. Math., 2013)

Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm. - Grzegorz Bancerek (Formaliz. Math., 2014)

Term Context. - Grzegorz Bancerek (Formaliz. Math., 2014)

Algebraic Approach to Algorithmic Logic. - Grzegorz Bancerek (Formaliz. Math., 2014)

Mizar: State-of-the-art and Beyond. - Grzegorz Bancerek; Czeslaw Bylinski; Adam Grabowski; Artur Kornilowicz; Roman Matuszewski; Adam Naumowicz; Karol Pak; Josef Urban (CICM, 2015)

On Multiset Ordering. - Grzegorz Bancerek (Formaliz. Math., 2016)

System Description: XSL-Based Translator of Mizar to LaTeX. - Grzegorz Bancerek; Adam Naumowicz; Josef Urban (CICM, 2018)

The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. - Grzegorz Bancerek; Czeslaw Bylinski; Adam Grabowski; Artur Kornilowicz; Roman Matuszewski; Adam Naumowicz; Karol Pak (J. Autom. Reason., 2018)