Enriching a Meta-Language With Higher-Order Features

Various meta-languages for the manipulation and specification of programs and programming languages have recently been proposed. We examine one such framework, called natural semantics, which was inspired by the work of G. Plotkin on operational semantics and extended by G. Kahn and others at INRIA. Natural semantics makes use of a first-order meta-language which represents programs as first-order tree structures and reasons about these using natural deduction-like methods. We present the following three enrichments of this meta-language. First, programs are represented not by first-order structures but by simply typed λ-terms. Second, schema variables in inference rules can be higher-order variables. Third, the reasoning mechanism is explicitly extended with proof methods which have proved valuable for natural deduction systems. In particular, we add methods for introducing and discharging assumptions and for introducing and discharging parameters. The first method can be used to prove hypothetical propositions while the second can be used to prove generic or universal propositions. We provide several example specifications using this extended meta-language and compare them to their first-order specifications. We argue that our extension yields a more natural and powerful meta-language than the related first-order system. We outline how this enriched meta-language can be compiled into the higher-order logic programming language λProlog