Implementing tactics and tacticals in a higher-order logic programming language

1993 ◽  
Vol 11 (1) ◽  
pp. 43-81 ◽  
Author(s):  
Amy Felty
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Logic Programming Language

Extended natural semantics

1993 ◽  
Vol 3 (2) ◽  
pp. 123-152 ◽  
Author(s):  
John Hannan
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Higher Order ◽  
Order Logic ◽  
Inference Rules ◽  
Abstract Syntax ◽  
Higher Order Logic ◽  
First Order ◽  
Definition Of

AbstractWe extend the definition of natural semantics to include simply typed λ-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call extended natural semantics, affords a higher-level notion of abstract syntax for representing programs and suitable mechanisms for manipulating this syntax. We present several examples of semantic specifications for a simple functional programming language and demonstrate how we achieve simple and elegant manipulations of bound variables in functional programs. All the examples have been implemented and tested in λProlog, a higher-order logic programming language that supports all of the features of extended natural semantics.

A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

2011 ◽  
Vol 76 (2) ◽  
pp. 673-699 ◽  
Author(s):  
Michael Gabbay
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Order Logic ◽  
First Order Logic ◽  
Cut Elimination ◽  
Logic Programming Language ◽  
First Order ◽  
Functional Programming Language ◽  
Sequent System

AbstractWe build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic.We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

Sign in / Sign up

Export Citation Format

Share Document