Theona.Stefanis@A.CS.CMU.EDU (02/05/86)
From: Theona Stefanis@A.CS.CMU.EDU JOINT LOGIC COLLOQUIUM (CMU, U of Pgh) Dale Miller CIS Department, University of Pennsylvania Date: Thursday February 13 Time: 3 pm Place: 4605 Wean Hall A Logic Programming Language Based on Intuitionistic Higher-Order Logic. Dale Miller CIS Department, University of Pennsylvania In this talk, we present a programming language whose operational semantics can be understood as searching for proofs with in a subset of intuitionistic higher-order logic. Kripke-models over a universe of higher-order terms provide a model theoretic semantics for our programs. Such models can be computed as least fix points. This logical language is a natural extension to Horn clause logic and the programming language based on it has many features not available in simple Horn clause based programming languages. In particular, this programming language can manipulate higher-order functions in a manner similar to many functional programming languages. An interesting notion of parametric modules is also available by virtue of the behavior of implication within an intuitionistic logic. An interpreter for this language must perform unification of higher-order terms. If time permits, we illustrate how this feature makes possible the very clean implementation of certain kinds of program transformation algorithms.