2012 · 30 citations · 36 references
ComputingComputer ScienceCompilersProgramming LanguagesSoftware EngineeringAbstract Syntax TreesCompiler ConstructionData-flow AnalysisFunctional ProgrammingSoftware RefactoringType SystemsCompiler DesignEquational LogicEquational ReasoningProgram OptimizationProgram TransformationTransformations
The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks. This paper introduces a programmatic and compiler-centric interface that facilitates refactoring and equational reasoning. To develop our ideas, we have implemented HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them.
36
A Transformation System for Developing Recursive Programs
R. M. Burstall, John Darlington · Journal of the ACM · 1977 · 1.3K citations · Full text
Template meta-programming for Haskell
Tim Sheard, Simon Peyton Jones · 2002 · 548 citations
The foundation of a generic theorem prover
Lawrence C. Paulson · Journal of Automated Reasoning · 1989 · 384 citations
Ralf Lämmel, Simon Peyton Jones · 2003 · 350 citations