Recursive Definitions in Type Theory. - Robert L. Constable; Nax Paul Mendler (Logic of Programs, 1985)

Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

Infinite Objects in Type Theory - Nax Paul Mendler; Prakash Panangaden; Robert L. Constable (LICS, 1986)

Recursive Types and Type Constraints in Second-Order Lambda Calculus - Nax Paul Mendler (LICS, 1987)

A Final Coalgebra Theorem. - Peter Aczel; Nax Paul Mendler (Category Theory and Computer Science, 1989)

Predicative Type Universes and Primitive Recursion - Nax Paul Mendler (LICS, 1991)

Inductive Types and Type Constraints in the Second-Order lambda Calculus. - Nax Paul Mendler (Ann. Pure Appl. Log., 1991)

A Logical View of Concurrent Constraint Programming. - Nax Paul Mendler; Prakash Panangaden; Philip J. Scott; Robert A. G. Seely (Nord. J. Comput., 1995)