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.

scholarly journals Set constraints for destructive array update optimization

2001 ◽  
Vol 11 (3) ◽  
pp. 319-346 ◽  
Author(s):  
MITCHELL WAND ◽  
WILLIAM D. CLINGER
Keyword(s):  
Polynomial Time ◽  
Program Transformation ◽  
Operational Semantics ◽  
Functional Languages ◽  
Small Step ◽  
Set Constraints ◽  
Correct Program

Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize and prove the soundness of these analyses using small-step operational semantics. We also prove that any sound liveness analysis induces a correct program transformation.

scholarly journals A Simple Correctness Proof of the Direct-Style Transformation

2002 ◽  
Vol 9 (2) ◽  
Author(s):  
Lasse R. Nielsen
Keyword(s):  
Program Transformation ◽  
Higher Order ◽  
Correctness Proof ◽  
First Order ◽  
Structural Induction ◽  
Higher Order Functions

We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on, e.g., a one-pass higher-order CPS transformation, and were complicated by having to reason about higher-order functions. In contrast, this work is based on a one-pass CPS transformation that is both compositional and first-order, and therefore the proof simply proceeds by structural induction on syntax.

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.

Sign in / Sign up

Export Citation Format

Share Document