A calculus with polymorphic and polyvariant flow types

2002 ◽  
Vol 12 (3) ◽  
pp. 183-227 ◽  
Author(s):  
J. B. WELLS ◽  
ALLYN DIMOCK ◽  
ROBERT MULLER ◽  
FRANKLYN TURBAK
Keyword(s):  
Programming Languages ◽  
Data Flow ◽  
Higher Order ◽  
Program Transformations ◽  
Optimizing Compilers ◽  
Intermediate Language ◽  
Program Representation ◽  
Key Innovation ◽  
Data Representations ◽  
Flow Information

We present λCIL, a typed λ-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of λCIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since λCIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.

scholarly journals Program Transformations in a Denotational Setting

1981 ◽  
Vol 10 (140) ◽  
Author(s):  
Flemming Nielson
Keyword(s):  
Data Flow ◽  
Weak Equivalence ◽  
Program Transformations ◽  
Optimizing Compilers ◽  
Flow Information

<p>Program transformations are frequently performed by optimizing compilers and the correctness of applying them usually depends on data flow information. For source-to-source transformations it is shown how a denotational setting can be useful for validating such program transformations.</p><p>Strong equivalence is obtained for transformations that exploit forward data flow information, whereas weak equivalence is obtained for transformations that exploit backward data flow information. To obtain strong equivalence both the original and the transformed program must be data flow analysed, but consideration of a transformation exploiting liveness of variables indicates that a more satisfactory approach may be possible.</p>

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.

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.

Sign in / Sign up

Export Citation Format

Share Document