Towards machine-checked compiler correctness for higher-order pure functional languages

1995 ◽  
pp. 369-381 ◽  
Author(s):  
David Lester ◽  
Sava Mintchev
Keyword(s):  
Higher Order ◽  
Functional Languages ◽  
Compiler Correctness

scholarly journals Compositional optimizations for CertiCoq

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Zoe Paraskevopoulou ◽  
John M. Li ◽  
Andrew W. Appel
Keyword(s):  
Difficult Problem ◽  
Higher Order ◽  
Additional Restriction ◽  
Logical Relation ◽  
Compositional Verification ◽  
Compiler Correctness ◽  
Separate Compilation ◽  
Proof Techniques ◽  
End To End ◽  
Program Components

Compositional compiler verification is a difficult problem that focuses on separate compilation of program components with possibly different verified compilers. Logical relations are widely used in proving correctness of program transformations in higher-order languages; however, they do not scale to compositional verification of multi-pass compilers due to their lack of transitivity. The only known technique to apply to compositional verification of multi-pass compilers for higher-order languages is parametric inter-language simulations (PILS), which is however significantly more complicated than traditional proof techniques for compiler correctness. In this paper, we present a novel verification framework for lightweight compositional compiler correctness . We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through the same sequence of intermediate representations , logical relation proofs can be transitively composed in order to derive an end-to-end compositional specification for multi-pass compiler pipelines. Unlike traditional logical-relation frameworks, our framework supports divergence preservation—even when transformations reduce the number of program steps. We achieve this by parameterizing our logical relations with a pair of relational invariants . We apply this technique to verify a multi-pass, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq’s specification language) to C. The pipeline optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can be easily code-generated to low-level languages. Notably, our pipeline performs more complex closure-allocation optimizations than the state of the art in verified compilation. Using our novel verification framework, we prove an end-to-end theorem for our pipeline that covers both termination and divergence and applies to whole-program and separate compilation, even when different modules are compiled with different optimizations. Our results are mechanized in the Coq proof assistant.

scholarly journals Applicative bidirectional programming

2018 ◽  
Vol 28 ◽  
Author(s):  
KAZUTAKA MATSUDA ◽  
MENG WANG
Keyword(s):  
Higher Order ◽  
Functional Languages ◽  
Bidirectional Transformation ◽  
Specialized Languages ◽  
Data Objects ◽  
Opening Up

AbstractA bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. One way to reduce the development and maintenance effort of bidirectional transformations is to have specialized languages in which the resulting programs are bidirectional by construction—giving rise to the paradigm of bidirectional programming. In this paper, we develop a framework for applicative-style and higher-order bidirectional programming, in which we can write bidirectional transformations as unidirectional programs in standard functional languages, opening up access to the bundle of language features previously only available to conventional unidirectional languages. Our framework essentially bridges two very different approaches of bidirectional programming, namely the lens framework and Voigtländer's semantic bidirectionalization, creating a new programming style that is able to obtain benefits from both.

Using transformations in the implementation of higher-order functions

1991 ◽  
Vol 1 (4) ◽  
pp. 459-494 ◽  
Author(s):  
Hanne Riis Nielson ◽  
Flemming Nielson
Keyword(s):  
Code Generation ◽  
Partial Evaluation ◽  
Current Trend ◽  
Higher Order ◽  
Functional Languages ◽  
Program Transformations ◽  
Time Level ◽  
Algebraic Laws ◽  
Polymorphic Type ◽  
Run Time

AbstractTraditional functional languages do not have an explicit distinction between binding times. It arises implicitly, however, as one typically instantiates a higher-order function with the arguments that are known, whereas the unknown arguments remain to be taken as parameters. The distinction between ‘known’ and ‘unknown’ is closely related to the distinction between binding times like ‘compile-time’ and ‘run-time’. This leads to the use of a combination of polymorphic type inference and binding time analysis for obtaining the required information about which arguments are known.Following the current trend in the implementation of functional languages we then transform the run-time level of the program (not the compile-time level) into categorical combinators. At this stage we have a natural distinction between two kinds of program transformations: partial evaluation, which involves the compile-time level of our notation, and algebraic transformations (i.e., the application of algebraic laws), which involves the run-time level of our notation.By reinterpreting the combinators in suitable ways we obtain specifications of abstract interpretations (or data flow analyses). In particular, the use of combinators makes it possible to use a general framework for specifying both forward and backward analyses. The results of these analyses will be used to enable program transformations that are not applicable under all circumstances.Finally, the combinators can also be reinterpreted to specify code generation for various (abstract) machines. To improve the efficiency of the code generated, one may apply abstract interpretations to collect extra information for guiding the code generation. Peephole optimizations may be used to improve the code at the lowest level.

scholarly journals Higher-order functional languages and intensional logic

1999 ◽  
Vol 9 (5) ◽  
pp. 527-564 ◽  
Author(s):  
P. RONDOGIANNIS ◽  
W. W. WADGE
Keyword(s):  
Broad Class ◽  
Higher Order ◽  
Final Outcome ◽  
Intensional Logic ◽  
New Technique ◽  
Functional Languages ◽  
Order Zero ◽  
Functional Program ◽  
Source Program ◽  
Context Manipulation

In this paper we demonstrate that a broad class of higher-order functional programs can be transformed into semantically equivalent multidimensional intensional programs that contain only nullary variable definitions. The proposed algorithm systematically eliminates user-defined functions from the source program, by appropriately introducing context manipulation (i.e. intensional) operators. The transformation takes place in M steps, where M is the order of the initial functional program. During each step the order of the program is reduced by one, and the final outcome of the algorithm is an M-dimensional intensional program of order zero. As the resulting intensional code can be executed in a purely tagged-dataflow way, the proposed approach offers a promising new technique for the implementation of higher-order functional languages.

Manipulating accumulative functions by swapping call-time and return-time computations

2012 ◽  
Vol 22 (3) ◽  
pp. 275-299
Author(s):  
AKIMASA MORIHATA ◽  
KAZUHIKO KAKEHI ◽  
ZHENJIANG HU ◽  
MASATO TAKEICHI
Keyword(s):  
Program Transformation ◽  
Return Time ◽  
Higher Order ◽  
Functional Languages ◽  
Recursive Functions ◽  
Program Inversion

AbstractFunctional languages are suitable for transformational developments of programs. However, accumulative functions, or in particular tail-recursive functions, are known to be less suitable for manipulation. In this paper, we propose a program transformation named “IO swapping” that swaps call-time and return-time computations. It moves computations in accumulative parameters to results and thereby enables interesting transformations. We demonstrate effectiveness of IO swapping by several applications: deforestation, higher order removal, program inversion, and manipulation of circular programs.

scholarly journals Oasis: An Optimizing Action-based Compiler Generator

1994 ◽  
Vol 13 (471) ◽  
Author(s):  
Peter Ørbæk
Keyword(s):  
Higher Order ◽  
Functional Languages ◽  
Optimizing Compilers ◽  
Action Semantics ◽  
Recursive Functions ◽  
Compiler Generation

Action Semantics is a new and interesting foundation for semantics based compiler generation. In this paper we present several analyses of actions, and apply them in a compiler generator capable of generating efficient, optimizing compilers for procedural and functional languages with higher order recursive functions. The automatically generated compilers produce code that is comparable with code produced by handwritten compilers.

Sign in / Sign up

Export Citation Format

Share Document