scholarly journals A Simple Take on Typed Abstract Syntax in Haskell-like Languages

2000 ◽  
Vol 7 (34) ◽  
Author(s):  
Olivier Danvy ◽  
Morten Rhiger
Keyword(s):  
Normal Forms ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Higher Order ◽  
Abstract Syntax ◽  
Typed Lambda Calculus

<p>We present a simple way to program typed abstract syntax in a <br />language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.</p><p>Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.</p>

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.

scholarly journals Normalization by Evaluation with Typed Abstract Syntax

2001 ◽  
Vol 8 (16) ◽  
Author(s):  
Olivier Danvy ◽  
Morten Rhiger ◽  
Kristoffer H. Rose
Keyword(s):  
Normal Forms ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Abstract Syntax ◽  
Type Checking

<p>We present a simple way to implement typed abstract syntax for the<br />lambda calculus in Haskell, using phantom types, and we specify <br />normalization by evaluation (i.e., type-directed partial evaluation) to yield this<br />typed abstract syntax. Proving that normalization by evaluation preserves<br /> types and yields normal forms then reduces to type-checking the<br />specification.</p>

scholarly journals A Complete Calculus of Monotone and Antitone Higher-Order Functions

10.29007/3n54 ◽  
2018 ◽  
Author(s):  
Thomas Icard ◽  
Lawrence Moss
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Higher Order ◽  
Typed Lambda Calculus ◽  
Higher Order Functions

This paper adds monotonicity and antitonicity information to the typed lambda calculus, thereby providing a foundation for the Monotonicity Calculus first developed by van Benthem and others. We establish properties of the type system, propose a syntax, semantics, and proof calculus, and prove completeness for the calculus with respect to hierarchies of monotone and antitone functions over base preorders.

scholarly journals A New One-Pass Transformation into Monadic Normal Form

2002 ◽  
Vol 9 (52) ◽  
Author(s):  
Olivier Danvy
Keyword(s):  
Normal Form ◽  
Symbolic Computation ◽  
Normal Forms ◽  
Lambda Calculus ◽  
Higher Order

We present a translation from the call-by-value lambda-calculus to monadic normal forms that includes short-cut boolean evaluation. The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly tail recursive. It makes a crucial use of symbolic computation at translation time.

A partial evaluator for the untyped lambda-calculus

1991 ◽  
Vol 1 (1) ◽  
pp. 21-69 ◽  
Author(s):  
Carsten K. Gomard ◽  
Neil D. Jones
Keyword(s):  
Input Data ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Higher Order ◽  
Residual Program ◽  
Source Program ◽  
Point Operator ◽  
Free Subset ◽  
Residual Code ◽  
Lambda Expression

AbstractThis article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously higher-order, non-trivial, and self-applicable.Partial evaluation produces aresidual programfrom a source program and some of its input data. When given the remaining input data the residual program yields the same result that the source program would when given all its input data. Our partial evaluator produces a residual lambda-expression given a source lambda-expression and the values of some of its free variables. By self-application, the partial evaluator can be used to compile and to generate stand-alone compilers from a denotational or interpretive specification of a programming language.An essential component in our self-applicable partial evaluator is the use of explicitbinding time information.We use this to annotate the source program, marking asresidualthe parts for which residual code is to be generated and marking aseliminablethe parts that can be evaluated using only the data that is known during partial evaluation. We give a simple criterion,well-annotatedness,that can be used to check that the partial evaluator can handle the annotated higher-order programs without committing errors.Our partial evaluator is simple, is implemented in a side-effect free subset of Scheme, and has been used to compile and to generate compilers and a compiler generator. In this article we examine two machine-generated compilers and find that their structures are surprisingly natural.

A Temporal-Logic Approach to Binding-Time Analysis

1995 ◽  
Vol 2 (51) ◽  
Author(s):  
Rowan Davies
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Time Analysis ◽  
Typed Lambda Calculus ◽  
Binding Time ◽  
Logic Approach ◽  
Multi Level ◽  
Binding Time Analysis

<p>The Curry-Howard isomorphism identifies proofs with typed lambda-<br />calculus terms, and correspondingly identifies propositions with<br />types. We show how this isomorphism can be extended to relate<br />constructive temporal logic with binding-time analysis. In particular,<br />we show how to extend the Curry-Howard isomorphism<br />to include the   ("next") operator from linear-time temporal<br />logic. This yields the simply typed lambda-calculus which we prove<br />to be equivalent to a multi-level binding-time analysis like those<br />used in partial evaluation.</p><p><br />Keywords: Curry-Howard isomorphism, partial evaluation, binding-time analysis, temporal logic.</p>

scholarly journals Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation (Preliminary Version)

1997 ◽  
Vol 4 (43) ◽  
Author(s):  
Vincent Balat ◽  
Olivier Danvy
Keyword(s):  
Normal Form ◽  
Virtual Machine ◽  
Code Generation ◽  
Normal Forms ◽  
Partial Evaluation ◽  
Higher Order ◽  
Time Code ◽  
Strong Normalization ◽  
Preliminary Version ◽  
Run Time

We investigate the synergy between type-directed partial evaluation and run-time code generation for the Caml dialect of ML. Type-directed partial evaluation maps simply typed, closed Caml values to a representation of their long beta-eta-normal form. Caml uses a virtual machine and has the capability to load byte code at run time. Representing the long beta-eta-normal forms as byte code gives us the ability to strongly normalize higher-order values (i.e., weak head normal forms in ML), to compile the resulting strong normal forms into byte code, and to load this byte code all in one go, at run time.<br />We conclude this note with a preview of our current work on scaling<br />up strong normalization by run-time code generation to the Caml<br />module language.

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

2004 ◽  
Vol 39 (1) ◽  
pp. 64-76 ◽  
Author(s):  
Vincent Balat ◽  
Roberto Di Cosmo ◽  
Marcelo Fiore
Keyword(s):  
Partial Evaluation ◽  
Lambda Calculus ◽  
Typed Lambda Calculus

scholarly journals RS-2 Tagging, Encoding, and Jones Optimality

2003 ◽  
Vol 10 (2) ◽  
Author(s):  
Olivier Danvy ◽  
Pablo E. Martínez López
Keyword(s):  
Partial Evaluation ◽  
Higher Order ◽  
The Self ◽  
Abstract Syntax ◽  
Original Source ◽  
Simple Representation ◽  
Residual Program ◽  
Source Program

A partial evaluator is said to be Jones-optimal if the result of specializing a self-interpreter with respect to a source program is textually identical to the source program, modulo renaming. Jones optimality has already been obtained if the self-interpreter is untyped. If the self-interpreter is typed, however, residual programs are cluttered with type tags. To obtain the original source program, these tags must be removed.<br /> <br />A number of sophisticated solutions have already been proposed. We observe, however, that with a simple representation shift, ordinary partial evaluation is already Jones-optimal, modulo an encoding. The representation shift amounts to reading the type tags as constructors for higher-order abstract syntax. We substantiate our observation by considering a typed self-interpreter whose input syntax is higher-order. Specializing this interpreter with respect to a source program yields a residual program that is textually identical to the source program, modulo renaming.

Sign in / Sign up

Export Citation Format

Share Document