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.

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.

Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod

10.29007/6shf ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Experimental Results ◽  
Relational Model ◽  
Finite Model ◽  
Higher Order Logic ◽  
First Order ◽  
Recursive Functions

Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model finder, it approximates infinite types by finite subsets. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order logic, without restrictions on the form of the formulas to falsify.

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.

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.

Sign in / Sign up

Export Citation Format

Share Document