Efficient Type Reconstruction in the Presence of Inheritance. - Marcin Benke (MFCS, 1993)

Predicative Polymorphic Subtyping. - Marcin Benke (MFCS, 1998)

An Algebraic Characterization of Typability in ML with Subtyping. - Marcin Benke (FoSSaCS, 1999)

Some Complexity Bounds for Subtype Inequalities. - Marcin Benke (Theor. Comput. Sci., 1999)

Universes for Generic Programs and Proofs in Dependent Type Theory. - Marcin Benke; Peter Dybjer; Patrik Jansson (Nord. J. Comput., 2003)

A Tool for Automated Theorem Proving in Agda. - Fredrik Lindblad; Marcin Benke (TYPES, 2004)

Verifying haskell programs using constructive type theory. - Andreas Abel 001; Marcin Benke; Ana Bove; John Hughes 001; Ulf Norell (Haskell, 2005)

Lucretia - a type system for objects in languages with reflection - Viviana Bono; Marcin Benke; Aleksy Schubert (CoRR, 2012)

Lucretia - intersection type polymorphism for scripting languages. - Marcin Benke; Viviana Bono; Aleksy Schubert (ITRS, 2014)

Specifying Functional Programs with Intuitionistic First Order Logic. - Marcin Benke (CS&P, 2015)

Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. - Marcin Benke; Aleksy Schubert; Daria Walukiewicz-Chrzaszcz (FSCD, 2016)