In Praise of Impredicativity: A Contribution to the Formalisation of
  Meta-Programming

There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

Abstract

Processing programs as data is one of the successes of functional and logic programming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logic programming, are widespread declarative programming techniques. In logic programming, there is a gap between the meta-programming practice and its theory: The formalisations of meta-programming do not explicitly address its impredicativity and are cumbersome. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former logics and by defining Reflective Predicate Logic, a conservative extension of first-order logic, that provides a simple formalisation of meta-programming. Under consideration for publication in Theory and Practice of Logic Programming

Related collections

Most cited references 13

Record: found
Abstract: found
Article: not found

A formulation of the simple theory of types

Alonzo Church (1940)

The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λx and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).