scholarly journals Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions

2007 ◽  
Vol 174 (7) ◽  
pp. 41-60
Author(s):  
Brigitte Pientka
Keyword(s):  
Functional Programming ◽  
Higher Order ◽  
Abstract Syntax ◽  
Explicit Substitutions

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.

scholarly journals Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs

10.29007/jqtz ◽  
2018 ◽  
Author(s):  
Nada Habli ◽  
Amy P. Felty
Keyword(s):  
Programming Languages ◽  
Automatic Generation ◽  
Higher Order ◽  
Specification Language ◽  
Proof Assistants ◽  
Abstract Syntax ◽  
Formal Systems ◽  
Ongoing Work ◽  
General Specification ◽  
Automated Proof

We describe ongoing work on building an environment to support reasoning in proof assistants that represent formal systems using higher-order abstract syntax (HOAS). We use a simple and general specification language whose syntax supports HOAS. Using this language, we can encode the syntax and inference rules of a variety of formal systems, such as programming languages and logics. We describe our tool, implemented in OCaml, which parses this syntax, and translates it to a Coq library that includes definitions and hints for aiding automated proof in the Hybrid system. Hybrid itself is implemented in Coq, and designed specifically to reason about such formal systems. Given an input specification, the library that is automatically generated by our tool imports the general Hybrid library and adds definitions and hints for aiding automated proof in Hybrid about the specific programming language or logic defined in the specification. This work is part of a larger project to compare reasoning in systems supporting HOAS. Our current work focuses on Hybrid, Abella, Twelf, and Beluga, and the specification language is designed to be general enough to allow the automatic generation of libraries for all of these systems from a single specification.

scholarly journals Higher Order Unification via Explicit Substitutions

2000 ◽  
Vol 157 (1-2) ◽  
pp. 183-235 ◽  
Author(s):  
Gilles Dowek ◽  
Thérèse Hardin ◽  
Claude Kirchner
Keyword(s):  
Higher Order ◽  
Explicit Substitutions

Principal signatures for higher-order program modules

1994 ◽  
Vol 4 (3) ◽  
pp. 285-335 ◽  
Author(s):  
Mads Tofte
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Higher Order ◽  
Principal Type ◽  
Functional Programming Languages ◽  
Standard Ml ◽  
Static Semantics ◽  
Program Modules

AbstractIn this paper we present a language for programming with higher-order modules. The language HML is based on Standard ML in that it provides structures, signatures and functors. In HML, functors can be declared inside structures and specified inside signatures; this is not possible in Standard ML. We present an operational semantics for the static semantics of HML signature expressions, with particular emphasis on the handling of sharing. As a justification for the semantics, we prove a theorem about the existence of principal signatures. This result is closely related to the existence of principal type schemes for functional programming languages with polymorphism.

scholarly journals Primitive recursion for higher-order abstract syntax

2001 ◽  
Vol 266 (1-2) ◽  
pp. 1-57 ◽  
Author(s):  
Carsten Schürmann ◽  
Joëlle Despeyroux ◽  
Frank Pfenning
Keyword(s):  
Higher Order ◽  
Abstract Syntax ◽  
Primitive Recursion

Mechanizing proofs with logical relations – Kripke-style

2018 ◽  
Vol 28 (9) ◽  
pp. 1606-1638 ◽  
Author(s):  
ANDREW CAVE ◽  
BRIGITTE PIENTKA
Keyword(s):  
Case Studies ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Higher Order ◽  
Abstract Syntax ◽  
Completeness Proof ◽  
Typed Lambda Calculus ◽  
Contextual Equivalence ◽  
The Right

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environmentBeluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs inBelugarelies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage ofBeluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploitBeluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate thatBelugaprovides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.

Sign in / Sign up

Export Citation Format

Share Document