publications: - title: "Proving correctness via free theorems: The case of the destroy/build-rule" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2008" doi: "http://doi.acm.org/10.1145/1328408.1328412" abstract: "Free theorems feature prominently in the field of program transformation for pure functional languages such as Haskell. However, somewhat disappointingly, the semantic properties of so based transformations are often established only very superficially. This paper is intended as a case study showing how to use the existing theoretical foundations and formal methods for improving the situation. To that end, we investigate the correctness issue for a new transformation rule in the short cut fusion family. This destroy/build-rule provides a certain reconciliation between the competing foldr/build- and destroy/unfoldr-approaches to eliminating intermediate lists. Our emphasis is on systematically and rigorously developing the rule's correctness proof, even while paying attention to semantic aspects like potential nontermination and mixed strict/nonstrict evaluation." links: doi: "http://doi.acm.org/10.1145/1328408.1328412" tags: - "programming languages" - "object-oriented programming" - "rule-based" - "case study" - "transformation language" - "functional programming" - "Haskell" - "rules" - "aspect oriented programming" - "systematic-approach" - "feature-oriented programming" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi08a" cites: 0 citedby: 0 pages: "13-20" booktitle: "PEPM" kind: "inproceedings" key: "Voi08a" - title: "Ideas for connecting inductive program synthesis and bidirectionalization" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2012" doi: "http://doi.acm.org/10.1145/2103746.2103757" abstract: "We share a vision of connecting the topics of bidirectional transformation and inductive program synthesis, by proposing to use the latter in approaching problematic aspects of the former. This research perspective does not present accomplished results, rather opening discussion and describing experiments designed to explore the potential of inductive program synthesis for bidirectionalization (the act of automatically producing a backwards from a forwards transformation), in particular to address the issue of integrating programmer intentions and expectations. " links: doi: "http://doi.acm.org/10.1145/2103746.2103757" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/Voigtlander12" researchr: "https://researchr.org/publication/Voigtlander12-0" cites: 0 citedby: 0 pages: "39-42" booktitle: "PEPM" kind: "inproceedings" key: "Voigtlander12-0" - title: "A family of syntactic logical relations for the semantics of Haskell-like languages" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" doi: "http://dx.doi.org/10.1016/j.ic.2007.11.009" abstract: "Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations." links: doi: "http://dx.doi.org/10.1016/j.ic.2007.11.009" tags: - "laziness" - "programming languages" - "semantics" - "rule-based" - "program analysis" - "pattern language" - "functional programming" - "analysis" - "Haskell" - "pattern matching" - "programming" researchr: "https://researchr.org/publication/JV09" cites: 0 citedby: 0 journal: "iandc" volume: "207" number: "2" pages: "341-368" kind: "article" key: "JV09" - title: "Composition of restricted Macro Tree Transducers" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2001" abstract: "A special class of functional programs can be modelled by Macro Tree Transducers. We present a technique that can be used to solve the efficiency problems due to creation and consumption of intermediate results in such functional programs, by constructing for two given Macro Tree Transducers, with appropriate restrictions, a single Macro Tree Transducer that implements the composition of the two original ones. We show that this is possible, if the first Macro Tree Transducer is non-copying and the second one is weakly single-use. Thus, we obtain the characterization MAC_nc;MAC_wsu=MAC, which generalizes a previous result. We also develop two post-processing constructions that can be used for optimizing the Macro Tree Transducer obtained from the composition construction, by eliminating superfluous context parameters and superfluous traversals through the input tree. Further, we present two interesting applications of the above characterization to problems about non-copying Macro Tree Transducers." links: successor: "https://researchr.org/publication/VK04" tags: - "optimization" - "macro" - "meta programming" - "meta-model" - "traversal" - "composition" - "functional programming" - "macros" - "context-aware" - "program optimization" - "Meta-Environment" - "process modeling" researchr: "https://researchr.org/publication/Voi01" cites: 0 citedby: 0 school: "Technische Universität Dresden" advisor: - name: "Armin Kühnemann" link: "http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/k/K=uuml=hnemann:Armin.html" - name: "Heiko Vogler" link: "http://www.inf.tu-dresden.de/index.php?node_id=1568&ln=en" kind: "mastersthesis" key: "Voi01" - title: "Much ado about two (pearl): A pearl on parallel prefix computation" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2008" doi: "http://doi.acm.org/10.1145/1328438.1328445" abstract: "This pearl develops a statement about parallel prefix computation in the spirit of Knuth's 0-1-Principle for oblivious sorting algorithms. It turns out that 0-1 is not quite enough here. The perfect hammer for the nails we are going to drive in is relational parametricity." links: doi: "http://doi.acm.org/10.1145/1328438.1328445" researchr: "https://researchr.org/publication/Voi08b" cites: 0 citedby: 0 pages: "29-35" booktitle: "POPL" kind: "inproceedings" key: "Voi08b" - title: "Proving Properties about Functions on Lists Involving Element Tests" author: - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-28412-0_17" abstract: "Bundy and Richardson (LPAR'99) developed a method for reasoning about functions manipulating lists which is based on separating shape from content, and then exploiting a mathematically convenient representation for expressing shape-only manipulations. Later, Prince et al. (FLOPS'08) extended the technique to other data structures, and gave it a more formal basis via the theory of containers. All these results are restricted to fully polymorphic functions. For example, functions using equality tests on list elements are out of reach. We remedy this situation by developing new abstractions and representations for less polymorphic functions. In Haskell speak, we extend the earlier approach to be applicable in the presence of (certain) type class constraints. " links: doi: "http://dx.doi.org/10.1007/978-3-642-28412-0_17" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/wadt/SeidelV10" researchr: "https://researchr.org/publication/SeidelV10" cites: 0 citedby: 0 pages: "270-286" booktitle: "WADT" kind: "inproceedings" key: "SeidelV10" - title: "Conditions for Efficiency Improvement by Tree Transducer Composition" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2378/23780222.htm" abstract: "We study the question of efficiency improvement or deterioration for a semantic-preserving program transformation technique based on macro tree transducer composition. By annotating functional programs to reflect the internal property ``computation time'' explicitly in the computed output, and by manipulating such annotations, we formally prove syntactic conditions under which the composed program is guaranteed to be more efficient than the original program, with respect to call-by-need reduction to normal form. The developed criteria can be checked automatically, and thus are suitable for integration into an optimizing functional compiler." links: doi: "http://link.springer.de/link/service/series/0558/bibs/2378/23780222.htm" successor: "https://researchr.org/publication/Voi07" tags: - "optimization" - "rule-based" - "composition" - "functional programming" - "macros" - "compiler" - "program optimization" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi02a" cites: 0 citedby: 0 pages: "222-236" booktitle: "RTA" kind: "inproceedings" key: "Voi02a" - title: "Free theorems for functional logic programs" author: - name: "Jan Christiansen" link: "http://korsika.informatik.uni-kiel.de/~jac/wordpress/" - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://doi.acm.org/10.1145/1707790.1707797" abstract: "Type-based reasoning is popular in functional programming. In particular, parametric polymorphism constrains functions in such a way that statements about their behavior can be derived without consulting function definitions. Is the same possible in a strongly, and polymorphically, typed functional logic language? This is the question we study in this paper. Logical features like nondeterminism and free variables cause interesting effects, which we examine based on examples and address by identifying appropriate conditions that guarantee standard free theorems or inequational versions thereof to hold. We see this case study as a stepping stone for a general theory, not provided here, involving the definition of a logical relation and other machinery required for parametricity arguments appropriate to functional logic languages." links: doi: "http://doi.acm.org/10.1145/1707790.1707797" tags: - "programming languages" - "rule-based" - "case study" - "functional programming" - " Curry" - "Haskell" - "relational parametricity" - "logic programming" - "programming" - "logic" - "type theory" researchr: "https://researchr.org/publication/CSV10" cites: 0 citedby: 0 pages: "39-48" booktitle: "plpv" kind: "inproceedings" key: "CSV10" - title: "Parametricity for Haskell with Imprecise Error Semantics" author: - name: "Florian Stenger" link: "http://www.simunova.com/node/129" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_22" abstract: "Error raising, propagation, and handling in Haskell can be imprecise in the sense that a language implementation's choice of local evaluation order, and optimizing transformations to apply, may influence which of a number of potential failure events hidden somewhere in a program is actually triggered. While this has pragmatic advantages from an implementation point of view, it also complicates the meaning of programs and thus requires extra care when reasoning about them. The proper semantic setup is one in which every erroneous value represents a whole set of potential (but not arbitrary) failure causes. The associated propagation rules are somewhat askew to standard notions of program flow and value dependence. As a consequence, standard reasoning techniques are cast into doubt, and rightly so. We study this issue in depth for one such reasoning technique, namely the derivation of free theorems from polymorphic types. We revise and extend the foundational notion of relational parametricity, as well as further material required to make it applicable." links: doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_22" tags: - "programming languages" - "optimization" - "semantics" - "rule-based" - "data-flow language" - "transformation language" - "Haskell" - "data-flow programming" - "data-flow" - "rules" - "program optimization" - "higher-order transformations" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/SV09a" cites: 0 citedby: 0 pages: "294-308" booktitle: "tlca" kind: "inproceedings" key: "SV09a" - title: "Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" - name: "Zhenjiang Hu" link: "http://research.nii.ac.jp/~hu/" - name: "Kazutaka Matsuda" link: "http://www.kb.ecei.tohoku.ac.jp/~kztk/" - name: "Meng Wang" link: "http://www.comlab.ox.ac.uk/people/meng.wang/" year: "2013" doi: "http://dx.doi.org/10.1017/S0956796813000130" abstract: "Matsuda et al. (ICFP 2007) and Voigtländer (POPL 2009) have introduced two techniques that given a source-to-view function provide an update propagation function mapping an original source and an updated view back to an updated source, subject to standard consistency conditions. Previously, we developed a synthesis of the two techniques, based on a separation of shape and content aspects (Voigtländer et al., ICFP 2010). Here, we carry that idea further, reworking the technique of Voigtländer such that any shape bidirectionalizer (based on the work of Matsuda et al. or not) can be used as a plug-in, to good effect. We also provide a data-type-generic account, enabling wider reuse, including the use of pluggable bidirectionalization itself as a plug-in. " links: doi: "http://dx.doi.org/10.1017/S0956796813000130" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/VoigtlanderHMW13" researchr: "https://researchr.org/publication/VoigtlanderHMW13" cites: 0 citedby: 0 journal: "JFP" volume: "23" number: "5" pages: "515-551" kind: "article" key: "VoigtlanderHMW13" - title: "Strictification of circular programs" author: - name: "João Paulo Fernandes" link: "http://wiki.di.uminho.pt/twiki/bin/view/Personal/Joao/" - name: "João Saraiva" link: "http://di.uminho.pt/~jas" - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2011" doi: "http://doi.acm.org/10.1145/1929501.1929526" abstract: "Circular functional programs (necessarily evaluated lazily) have been used as algorithmic tools, as attribute grammar implementations, and as target for program transformation techniques. Classically, Richard Bird [1984] showed how to transform certain multitraversal programs (which could be evaluated strictly or lazily) into one-traversal ones using circular bindings. Can we go the other way, even for programs that are not in the image of his technique? That is the question we pursue in this paper. We develop an approach that on the one hand lets us deal with typical examples corresponding to attribute grammars, but on the other hand also helps to derive new algorithms for problems not previously in reach." links: doi: "http://doi.acm.org/10.1145/1929501.1929526" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/FernandesSSV11" tags: - "laziness" - "attribute grammars" - "traversal" - "functional programming" - "programming" - "systematic-approach" - "transformation" - "grammar" - "program transformation" researchr: "https://researchr.org/publication/FernandesSSV11" cites: 0 citedby: 0 pages: "131-140" booktitle: "PEPM" kind: "inproceedings" key: "FernandesSSV11" - title: "Free theorems involving type constructor classes (functional pearl)" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" doi: "http://doi.acm.org/10.1145/1596550.1596577" abstract: "Free theorems are a charm, allowing the derivation of useful statements about programs from their (polymorphic) types alone. We show how to reap such theorems not only from polymorphism over ordinary types, but also from polymorphism over type constructors restricted by class constraints. Our prime application area is that of monads, which form the probably most popular type constructor class of Haskell. To demonstrate the broader scope, we also deal with a transparent way of introducing difference lists into a program, endowed with a neat and general correctness proof." links: doi: "http://doi.acm.org/10.1145/1596550.1596577" tags: - "functional programming" - "constraints" - "Haskell" researchr: "https://researchr.org/publication/Voi09b" cites: 0 citedby: 0 pages: "173-184" booktitle: "ICFP" kind: "inproceedings" key: "Voi09b" - title: "Combining syntactic and semantic bidirectionalization" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" - name: "Zhenjiang Hu" link: "http://research.nii.ac.jp/~hu/" - name: "Kazutaka Matsuda" link: "http://www.kb.ecei.tohoku.ac.jp/~kztk/" - name: "Meng Wang" link: "http://www.comlab.ox.ac.uk/people/meng.wang/" year: "2010" doi: "http://doi.acm.org/10.1145/1863543.1863571" abstract: "Matsuda et al. [2007, ICFP] and Voigtländer [2009, POPL] introduced two techniques that given a source-to-view function provide an update propagation function mapping an original source and an updated view back to an updated source, subject to standard consistency conditions. Being fundamentally different in approach, both techniques have their respective strengths and weaknesses. Here we develop a synthesis of the two techniques to good effect. On the intersection of their applicability domains we achieve more than what a simple union of applying the techniques side by side delivers." links: doi: "http://doi.acm.org/10.1145/1863543.1863571" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/VoigtlanderHMW10" tags: - "source-to-source" - "consistency" - "systematic-approach" - "open-source" researchr: "https://researchr.org/publication/VoigtlanderHMW10" cites: 0 citedby: 0 pages: "181-192" booktitle: "ICFP" kind: "inproceedings" key: "VoigtlanderHMW10" - title: "Understanding idiomatic traversals backwards and forwards" author: - name: "Richard S. Bird" link: "http://www.comlab.ox.ac.uk/people/Richard.Bird/" - name: "Jeremy Gibbons" link: "http://www.comlab.ox.ac.uk/jeremy.gibbons/" - name: "Stefan Mehner" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1467.html" - name: "Tom Schrijvers" link: "http://users.ugent.be/~tschrijv" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2013" doi: "http://doi.acm.org/10.1145/2503778.2503781" abstract: "We present new ways of reasoning about a particular class of effectful Haskell programs, namely those expressed as idiomatic traversals. Starting out with a specific problem about labelling and unlabelling binary trees, we extract a general inversion law, applicable to any monad, relating a traversal over the elements of an arbitrary traversable type to a traversal that goes in the opposite direction. This law can be invoked to show that, in a suitable sense, unlabelling is the inverse of labelling. The inversion law, as well as a number of other properties of idiomatic traversals, is a corollary of a more general theorem characterising traversable functors as finitary containers: an arbitrary traversable object can be decomposed uniquely into shape and contents, and traversal be understood in terms of those. Proof of the theorem involves the properties of traversal in a special idiom related to the free applicative functor." links: doi: "http://doi.acm.org/10.1145/2503778.2503781" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/BirdGMVS13" researchr: "https://researchr.org/publication/BirdGMVS13" cites: 0 citedby: 0 pages: "25-36" booktitle: "haskell" kind: "inproceedings" key: "BirdGMVS13" - title: "First International Workshop on Bidirectional Transformations (BX 2012): Preface" author: - name: "Frank Hermann" link: "http://wwwen.uni.lu/snt/people/frank_hermann" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2012" doi: "http://journal.ub.tu-berlin.de/eceasst/article/view/733" links: doi: "http://journal.ub.tu-berlin.de/eceasst/article/view/733" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/eceasst/HermannV12" researchr: "https://researchr.org/publication/HermannV12" cites: 0 citedby: 0 journal: "eceasst" volume: "49" kind: "article" key: "HermannV12" - title: "Taming Selective Strictness" author: - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" abstract: "Free theorems establish interesting properties of parametrically polymorphic functions, solely from their types, and serve as a nice proof tool. For pure and lazy functional programming languages, they can be used with very few preconditions. Unfortunately, in the presence of selective strictness, as provided in languages like Haskell, their original strength is reduced. In this paper we present an approach for restrengthening them. By a refined type system which tracks the use of strict evaluation, we rule out unnecessary restrictions that otherwise emerge from the general suspicion that strict evaluation may be used at any point. Additionally, we provide an implemented algorithm determining all refined types for a given term." links: successor: "https://researchr.org/publication/SeidelV11" tags: - "laziness" - "programming languages" - "rule-based" - "functional programming" - "Haskell" - "type system" - "rules" - "programming" - "systematic-approach" researchr: "https://researchr.org/publication/SV09" cites: 0 citedby: 0 pages: "2916-2930" booktitle: "gi" kind: "inproceedings" key: "SV09" - title: "Deaccumulation techniques for improving provability" author: - name: "Jürgen Giesl" link: "http://verify.rwth-aachen.de/giesl/" - name: "Armin Kühnemann" link: "http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/k/K=uuml=hnemann:Armin.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2007" doi: "http://dx.doi.org/10.1016/j.jlap.2006.11.001" abstract: "Several induction theorem provers were developed to verify functional programs mechanically. Unfortunately, automatic verification often fails for functions with accumulating arguments. Using concepts from the theory of tree transducers and extending on earlier work, the paper develops automatic transformations from accumulative functional programs into non-accumulative ones, which are much better suited for mechanized verification. The overall goal is to reduce the need for generalizing induction hypotheses in (semi-)automatic provers. Via the correspondence between imperative programs and tail-recursive functions, the presented approach can also help to reduce the need for inventing loop invariants in the verification of imperative programs." links: doi: "http://dx.doi.org/10.1016/j.jlap.2006.11.001" tags: - "program verification" - "functional programming" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/GKV07" cites: 0 citedby: 0 journal: "jlp" volume: "71" number: "2" pages: "79-113" kind: "article" key: "GKV07" - title: "Formal Efficiency Analysis for Tree Transducer Composition" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2007" doi: "http://dx.doi.org/10.1007/s00224-006-1235-9" abstract: "We study the question of efficiency improvement or deterioration for a semantics-preserving program transformation technique for (lazy) functional languages, based on composition of restricted macro tree transducers. By annotating programs to reflect the intensional property ``computation time'' explicitly in the computed output and by manipulating such annotations, we formally prove syntactic conditions under which the composed program is guaranteed to be not less efficient than the original program with respect to the number of call-by-need reduction steps required to reach normal form. The criteria developed can be checked automatically and efficiently, and thus are suitable for integration into an optimizing compiler." links: doi: "http://dx.doi.org/10.1007/s00224-006-1235-9" tags: - "laziness" - "programming languages" - "optimization" - "semantics" - "rule-based" - "program analysis" - "formal semantics" - "transformation language" - "composition" - "functional programming" - "analysis" - "macros" - "compiler" - "program optimization" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi07" cites: 0 citedby: 0 journal: "mst" volume: "41" number: "4" pages: "619-689" kind: "article" key: "Voi07" - title: "Selective strictness and parametricity in structural operational semantics, inequationally" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2007" doi: "http://dx.doi.org/10.1016/j.tcs.2007.09.014" abstract: "Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. The formal background of such `free theorems' is well developed for extensions of the Girard-Reynolds polymorphic lambda calculus by algebraic datatypes and general recursion, provided the resulting calculus is endowed with either a purely strict or a purely nonstrict semantics. But modern functional languages like Clean and Haskell, while using nonstrict evaluation by default, also provide means to enforce strict evaluation of subcomputations at will. The resulting selective strictness gives the advanced programmer explicit control over evaluation order, but is not without semantic consequences: it breaks standard parametricity results. This paper develops an operational semantics for a core calculus supporting all the language features emphasized above. Its main achievement is the characterization of observational approximation with respect to this operational semantics via a carefully constructed logical relation. This establishes the formal basis for new parametricity results, as illustrated by several example applications, including the first complete correctness proof for short cut fusion in the presence of selective strictness. The focus on observational approximation, rather than equivalence, allows a finer-grained analysis of computational behavior in the presence of selective strictness than would be possible with observational equivalence alone." links: doi: "http://dx.doi.org/10.1016/j.tcs.2007.09.014" tags: - "programming languages" - "semantics" - "program analysis" - "completeness" - "formal semantics" - " structural operational semantics" - "functional programming" - "analysis" - "Haskell" - " algebra" - "operational semantics" researchr: "https://researchr.org/publication/VJ07%3A1" cites: 0 citedby: 0 journal: "TCS" volume: "388" number: "1-3" pages: "290-318" kind: "article" key: "VJ07:1" - title: "Semantics and Pragmatics of New Shortcut Fusion Rules" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2008" doi: "http://dx.doi.org/10.1007/978-3-540-78969-7_13" abstract: "We study various shortcut fusion rules for languages like Haskell. Following a careful semantic account of a recently proposed rule for circular program transformation, we propose a new rule that trades circularity for higher-orderedness, and thus attains better semantic properties. This also leads us to revisit the original foldr/build-rule, as well as its dual, and to develop variants that do not suffer from detrimental impacts of Haskell's mixed strict/nonstrict semantics. Throughout, we offer pragmatic insights about our new rules to investigate also their relative effectiveness, rather than just their semantic correctness." links: doi: "http://dx.doi.org/10.1007/978-3-540-78969-7_13" tags: - "programming languages" - "semantics" - "rule-based" - "transformation language" - "Haskell" - "rules" - "higher-order transformations" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi08c" cites: 0 citedby: 0 pages: "163-179" booktitle: "FLOPS" kind: "inproceedings" key: "Voi08c" - title: "A Generic Operational Metatheory for Algebraic Effects" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Alex Simpson" link: "http://homepages.inf.ed.ac.uk/als/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2010.29" abstract: "We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of algebraic effects, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power’s structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive “basic preorder” on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity." links: doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2010.29" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/JohannSV10" tags: - "programming languages" - "semantics" - "program analysis" - "generic programming" - " structural operational semantics" - "relational algebra" - "analysis" - "metatheory" - " algebra" - "programming" - "operational semantics" - "context-aware" - "systematic-approach" researchr: "https://researchr.org/publication/JSV10" cites: 0 citedby: 0 pages: "209-218" booktitle: "lics" kind: "inproceedings" key: "JSV10" - title: "An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry" author: - name: "Jan Christiansen" link: "http://korsika.informatik.uni-kiel.de/~jac/wordpress/" - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-20775-4_7" abstract: "With the aim of putting type-based reasoning for functional logic languages, as recently explored by Christiansen et al. (PLPV 2010), on a formal basis, we develop a denotational semantics for a typed core language of Curry. Dealing with the core language FlatCurry rather than with full Curry suffices, since there exists a type-preserving translation from the latter into the former. In contrast to existing semantics for functional logic languages, we deliberately approach the problem \"from the functional side\". That is, rather than adapting approaches previously known from the study of (resolution-like) semantics for logic languages, we aim for a semantics in the spirit of standard denotational semantics for the polymorphic lambda calculus. We claim and set out to prove that the presented semantics is adequate with respect to an existing operational semantics. A particularly interesting aspect, we think, is that we give the first denotational treatment of recursive let-bindings in combination with call-time choice." links: doi: "http://dx.doi.org/10.1007/978-3-642-20775-4_7" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/wflp/ChristiansenSV10" researchr: "https://researchr.org/publication/ChristiansenSV10" cites: 0 citedby: 0 pages: "119-136" booktitle: "wflp" kind: "inproceedings" key: "ChristiansenSV10" - title: "Free theorems for functional logic programs: (abstract only)" author: - name: "Jan Christiansen" link: "http://korsika.informatik.uni-kiel.de/~jac/wordpress/" - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" doi: "http://doi.acm.org/10.1145/1816027.1816035" abstract: "Type-based reasoning is popular in functional programming. In particular, parametric polymorphism constrains functions in such a way that statements about their behavior can be derived without consulting function definitions. Is the same possible in a strongly, and polymorphically, typed functional logic language? This is the question we study in this paper. Logical features like nondeterminism and free variables cause interesting effects, which we examine based on examples and address by identifying appropriate conditions that guarantee standard free theorems or inequational versions thereof to hold. We see this case study as a stepping stone for a general theory, not provided here, involving the definition of a logical relation and other machinery required for parametricity arguments appropriate to functional logic languages." links: doi: "http://doi.acm.org/10.1145/1816027.1816035" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/sigplan/ChristiansenSV09" successor: "https://researchr.org/publication/CSV10" researchr: "https://researchr.org/publication/ChristiansenSV09" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "44" number: "11" pages: "7" kind: "article" key: "ChristiansenSV09" - title: "The Impact of seq on Free Theorems-Based Program Transformations" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2006" doi: "http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=69&issue=1&spage=63" abstract: "Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results --- including so-called free theorems --- fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to ``inequational'' versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq." links: doi: "http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=69&issue=1&spage=63" tags: - "programming languages" - "rule-based" - "transformation language" - "functional programming" - "Haskell" - " algebra" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/JV06" cites: 0 citedby: 0 journal: "FUIN" volume: "69" number: "1-2" pages: "63-102" kind: "article" key: "JV06" - title: "Refined typing to localize the impact of forced strictness on free theorems" author: - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2011" doi: "http://dx.doi.org/10.1007/s00236-011-0136-9" abstract: "Free theorems establish interesting properties of parametrically polymorphic functions, solely from their types, and serve as a nice proof tool. For pure and lazy functional programming languages, they can be used with very few preconditions. Unfortunately, in the presence of selective strictness, as provided in languages like Haskell, their original strength is reduced. In this paper we present an approach for overcoming this weakness in specific situations. Employing a refined type system which tracks the use of enforced strict evaluation, we rule out unnecessary restrictions that otherwise emerge. Additionally, we provide (and implement) an algorithm determining all refined types for a given term." links: doi: "http://dx.doi.org/10.1007/s00236-011-0136-9" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/acta/SeidelV11" tags: - "laziness" - "programming languages" - "rule-based" - "functional programming" - "Haskell" - "type system" - "rules" - "programming" - "systematic-approach" - "domain-specific language" researchr: "https://researchr.org/publication/SeidelV11" cites: 0 citedby: 0 journal: "ACTA" volume: "48" number: "3" pages: "191-211" kind: "article" key: "SeidelV11" - title: "Using Circular Programs to Deforest in Accumulating Parameters" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2004" doi: "http://dx.doi.org/10.1023/B:LISP.0000029450.36668.cb" abstract: "This paper presents a functional program transformation that removes intermediate data structures in compositions of two members of a class of recursive functions with accumulating parameters. To avoid multiple traversals of the input data structure, the composition algorithm produces circular programs that make essential use of lazy evaluation and local recursion. The resulting programs are simplified using a post-processing phase sketched in the paper. The presented transformation, called lazy composition, is compared with related transformation techniques both on a qualitative level and based on runtime measurements. An alternative use of higher-orderedness instead of circularity is also briefly explored." links: doi: "http://dx.doi.org/10.1023/B:LISP.0000029450.36668.cb" tags: - "laziness" - "rule-based" - "traversal" - "composition" - "functional programming" - "data-flow programming" - "data-flow" - "programming" - "higher-order transformations" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi04a" cites: 0 citedby: 0 journal: "lisp" volume: "17" number: "1-2" pages: "129-163" kind: "article" key: "Voi04a" - title: "5. Arbeitstagung Programmiersprachen (ATPS 2012)" author: - name: "Frank Huch" link: "http://www-ps.informatik.uni-kiel.de/~fhu/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2012" doi: "http://subs.emis.de/LNI/Proceedings/Proceedings198/article6634.html" links: doi: "http://subs.emis.de/LNI/Proceedings/Proceedings198/article6634.html" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/se/HuchV12" researchr: "https://researchr.org/publication/HuchV12" cites: 0 citedby: 0 pages: "195" booktitle: "se" kind: "inproceedings" key: "HuchV12" - title: "Bidirectionalization for free! (Pearl)" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" doi: "http://doi.acm.org/10.1145/1480881.1480904" abstract: "A bidirectional transformation consists of a function get that takes a source (document or value) to a view and a function put that takes an updated view and the original source back to an updated source, governed by certain consistency conditions relating the two functions. Both the database and programming language communities have studied techniques that essentially allow a user to specify only one of get and put and have the other inferred automatically. All approaches so far to this bidirectionalization task have been syntactic in nature, either proposing a domain-specific language with limited expressiveness but built-in (and composable) backward components, or restricting get to a simple syntactic form from which some algorithm can synthesize an appropriate definition for put. Here we present a semantic approach instead. The idea is to take a general-purpose language, Haskell, and write a higher-order function that takes (polymorphic) get-functions as arguments and returns appropriate put-functions. All this on the level of semantic values, without being willing, or even able, to inspect the definition of get, and thus liberated from syntactic restraints. Our solution is inspired by relational parametricity and uses free theorems for proving the consistency conditions. It works beautifully." links: doi: "http://doi.acm.org/10.1145/1480881.1480904" tags: - "programming languages" - "model-to-model transformation" - "bidirectional model transformations" - "bidirectional transformation" - "relational database" - "bidirectional model transformation" - "transformation language" - "Haskell" - "source-to-source" - "model transformation" - "consistency" - "programming" - "database" - "higher-order transformations" - "systematic-approach" - "open-source" - "transformation" - "program transformation" - "domain-specific language" researchr: "https://researchr.org/publication/Voi09a" cites: 0 citedby: 0 pages: "165-176" booktitle: "POPL" kind: "inproceedings" key: "Voi09a" - title: "Free theorems in the presence of seq" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2004" doi: "http://doi.acm.org/10.1145/964001.964010" abstract: "Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, the standard parametricity theorem fails for nonstrict languages supporting a polymorphic strict evaluation primitive like Haskell's seq. Contrary to the folklore surrounding seq and parametricity, we show that not even quantifying only over strict and bottom-reflecting relations in the forall-clause of the underlying logical relation --- and thus restricting the choice of functions with which such relations are instantiated to obtain free theorems to strict and total ones --- is sufficient to recover from this failure. By addressing the subtle issues that arise when propagating up the type hierarchy restrictions imposed on a logical relation in order to accommodate the strictness primitive, we provide a parametricity theorem for the subset of Haskell corresponding to a Girard-Reynolds-style calculus with fixpoints, algebraic datatypes, and seq. A crucial ingredient of our approach is the use of an asymmetric logical relation, which leads to ``inequational'' versions of free theorems enriched by preconditions guaranteeing their validity in the described setting. Besides the potential to obtain corresponding preconditions for standard equational free theorems by combining some new inequational ones, the latter also have value in their own right, as is exemplified with a careful analysis of seq's impact on familiar program transformations." links: doi: "http://doi.acm.org/10.1145/964001.964010" successor: "https://researchr.org/publication/JV06" tags: - "programming languages" - "program analysis" - "transformation language" - "functional programming" - "analysis" - "Haskell" - " algebra" - "higher-order transformations" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/JV04" cites: 0 citedby: 0 pages: "99-110" booktitle: "POPL" kind: "inproceedings" key: "JV04" - title: "Three Complementary Approaches to Bidirectional Programming" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Kazutaka Matsuda" link: "http://www.kb.ecei.tohoku.ac.jp/~kztk/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-32202-0_1" abstract: "This paper surveys three distinct approaches to bidirectional programming. The first approach, syntactic bidirectionalization, takes a program describing the forward transformation as input and calculates a well-behaved reverse transformation. The second approach, semantic bidirectionalization, is similar, but takes the forward transformation itself as input rather than a program describing it. It requires the transformation to be a polymorphic function and uses parametricity and free theorems in the proof of well-behavedness. The third approach, based on bidirectional combinators, focuses on the use of types to ensure well-behavedness and special constructs for dealing with alignment problems. In presenting these approaches, we pay particular attention to use of complements, which are structures that represent the information discarded by the transformation in the forward direction. " links: doi: "http://dx.doi.org/10.1007/978-3-642-32202-0_1" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ssgip/FosterMV10" researchr: "https://researchr.org/publication/FosterMV10" cites: 0 citedby: 0 pages: "1-46" booktitle: "ssgip" kind: "inproceedings" key: "FosterMV10" - title: "Automatically Generating Counterexamples to Naive Free Theorems" author: - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-12251-4_14" abstract: "Disproof can be as important as proof in studying programs and programming languages. In particular, side conditions in a statement about program behavior are sometimes best understood and explored by trying to exhibit a falsifying example in the absence of a condition in question. Automation is as desirable for such falsification as it is for verification. We develop formal and implemented tools for counterexample generation in the context of free theorems, i.e., statements derived from polymorphic types a la relational parametricity. The machinery we use is rooted in constraining the type system and in intuitionistic proof search." links: doi: "http://dx.doi.org/10.1007/978-3-642-12251-4_14" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/flops/SeidelV10" tags: - "programming languages" - "type system" - "programming" - "context-aware" - "search" researchr: "https://researchr.org/publication/SV10" cites: 0 citedby: 0 pages: "175-190" booktitle: "FLOPS" kind: "inproceedings" key: "SV10" - title: "Asymptotic Improvement of Computations over Free Monads" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2008" doi: "http://dx.doi.org/10.1007/978-3-540-70594-9_20" abstract: "We present a low-effort program transformation to improve the efficiency of computations over free monads in Haskell. The development is calculational and carried out in a generic setting, thus applying to a variety of datatypes. An important aspect of our approach is the utilisation of type class mechanisms to make the transformation as transparent as possible, requiring no restructuring of code at all. There is also no extra support necessary from the compiler (apart from an up-to-date type checker). Despite this simplicity of use, our technique is able to achieve true asymptotic runtime improvements. We demonstrate this by examples for which the complexity is reduced from quadratic to linear." links: doi: "http://dx.doi.org/10.1007/978-3-540-70594-9_20" tags: - "generic programming" - "Haskell" - "compiler" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi08d" cites: 0 citedby: 0 pages: "388-403" booktitle: "mpc" kind: "inproceedings" key: "Voi08d" - title: "Programming language approaches to bidirectional transformation (invited talk)" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2012" doi: "http://doi.acm.org/10.1145/2427048.2427049" abstract: "Bidirectional transformations are pairs of transformations going back and forth between two data domains, possibly taking extra information into account to disambiguate in one or both directions, while being governed by certain consistency conditions. Application scenarios are view-update propagation in databases, model-driven engineering, and programming environments like structured editors, among others. Consequently, diverse disciplines contribute to the interest and development in this area. We focus on approaches that, rather than being centered on the data, take the involved transformations seriously as programs to analyze and manipulate." links: doi: "http://doi.acm.org/10.1145/2427048.2427049" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ldta/Voigtlander12" researchr: "https://researchr.org/publication/Voigtlander12" cites: 0 citedby: 0 pages: "1" booktitle: "LDTA" kind: "inproceedings" key: "Voigtlander12" - title: "Editorial" author: - name: "John P. Gallagher" link: "http://akira.ruc.dk/~jpg/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://dx.doi.org/10.1007/s10990-011-9081-0" links: doi: "http://dx.doi.org/10.1007/s10990-011-9081-0" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lisp/GallagherV10" researchr: "https://researchr.org/publication/GallagherV10" cites: 0 citedby: 0 journal: "lisp" volume: "23" number: "3" pages: "273-274" kind: "article" key: "GallagherV10" - title: "Concatenate, reverse and map vanish for free" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2002" doi: "http://doi.acm.org/10.1145/581478.581481" abstract: "We introduce a new transformation method to eliminate intermediate data structures occurring in functional programs due to repeated list concatenations and other data manipulations (additionally exemplified with list reversal and mapping of functions over lists). The general idea is to uniformly abstract from data constructors and manipulating operations by means of rank-2 polymorphic combinators that exploit algebraic properties of these operations to provide an optimized implementation. The correctness of transformations is proved by using the free theorems derivable from parametric polymorphic types." links: doi: "http://doi.acm.org/10.1145/581478.581481" tags: - "optimization" - "functional programming" - "data-flow programming" - "data-flow" - " algebra" - "program optimization" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi02c" cites: 0 citedby: 0 pages: "14-25" booktitle: "ICFP" kind: "inproceedings" key: "Voi02c" - title: "Composition of functions with accumulating parameters" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" - name: "Armin Kühnemann" link: "http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/k/K=uuml=hnemann:Armin.html" year: "2004" doi: "http://dx.doi.org/10.1017/S0956796803004933" abstract: "Many functional programs with accumulating parameters are contained in the class of macro tree transducers. We present a program transformation technique that can be used to solve the efficiency problems due to creation and consumption of intermediate data structures in compositions of such functions, where classical deforestation techniques fail. To do so, given two macro tree transducers under appropriate restrictions, we construct a single macro tree transducer that implements the composition of the two original ones. The imposed restrictions are more liberal than those in the literature on macro tree transducer composition, thus generalising previous results." links: doi: "http://dx.doi.org/10.1017/S0956796803004933" tags: - "composition" - "functional programming" - "macros" - "data-flow programming" - "data-flow" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/VK04" cites: 0 citedby: 0 journal: "JFP" volume: "14" number: "3" pages: "317-363" kind: "article" key: "VK04" - title: "Formalizing Semantic Bidirectionalization with Dependent Types" author: - name: "Helmut Grohne" link: "https://researchr.org/alias/helmut-grohne" - name: "Andres Löh" link: "http://people.cs.uu.nl/andres/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2014" doi: "http://ceur-ws.org/Vol-1133/paper-12.pdf" links: doi: "http://ceur-ws.org/Vol-1133/paper-12.pdf" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/edbt/GrohneLV14" researchr: "https://researchr.org/publication/GrohneLV14" cites: 0 citedby: 0 pages: "75-81" booktitle: "edbt" kind: "inproceedings" key: "GrohneLV14" - title: "Vorwort zur 6. Arbeitstagung Programmiersprachen (ATPS 2013)" author: - name: "Jens Knoop" link: "http://www.complang.tuwien.ac.at/knoop/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2013" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/se/KnoopV13a" researchr: "https://researchr.org/publication/KnoopV13a" cites: 0 citedby: 0 pages: "17-20" booktitle: "se" kind: "inproceedings" key: "KnoopV13a" - title: "Types for Programming and Reasoning" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2008" abstract: "Types play an increasingly important role in program construction, software engineering, and reasoning about programs. They serve as documentation of functionality, even as partial specifications, and can help to rule out whole classes of errors before a program is ever run. This provides qualitative guarantees and enables safe reuse of code components. In particular, static type checking constitutes a limited form of automatic correctness proof below the threshold of full, and undecidable, program verification. An important asset for maintaining a strong type discipline, which attempts to prevent the use of code in unfit contexts by assigning types that are as precise and descriptive as possible, without forgoing the goal of also flexible reuse is the availability of polymorphism, first identied as a distinct concept by Strachey (1967). A polymorphic type, or type scheme, expresses that a certain functionality is offered for different concrete type instantiations, and that in a controlled fashion. Even though the prospects of strong typing as a lightweight yet powerful formal method have already begun to influence the design of mainstream programming languages, and in particular Java and C# are embracing ever more sophisticated forms of polymorphism (Naftalin and Wadler 2006, Golding 2005), the real stronghold of typeful programming is in the area of functional programming languages like ML (Milner et al. 1997) and Haskell (Peyton Jones 2003). To some degree this may be an almost incidental consequence of the origin of much of the initial research into expressive types (Cardelli and Wegner 1985), but there are also profound reasons. The clear mathematical basis of the functional paradigm makes languages adhering to it particularly amenable to precise analysis and thus allows the formalization and mastery, both theoretically and practically, of very potent type systems. In fact, one of the defining characteristics of Haskell over the last two decades has been its role as a highly effective laboratory in which to explore, design, and implement advanced type-related ideas (Hudak et al. 2007). So the forefront of type research is still in the field of functional programming, and it is also this setting in which the work reported on in this thesis explores ways of using types for high-level program construction and reasoning about the behavior of programs. Specifically, a very nice synergy arises from Haskell's type discipline and Haskell's insistence on being a pure, rather than just any other \"almost\", functional language. The \"no compromises\" attitude vis-a-vis any impulse to relax the compliance with the mathematical concept of side-effect-free functions contributes to the existence of powerful reasoning techniques that connect the types of functions to those functions' possible observable behaviors. One such technique is the systematic derivation of statements about program behavior from (polymorphic) types alone. Originating from Reynolds' (1983) characterization of what it means, abstractly, for a function to be fully polymorphic over some part of its type, this approach has been popularized by Wadler (1989) under the slogan of \"free theorems\". It combines fruitfully with algebraic techniques like equational reasoning. One prominent application area for free theorems has been, and continues to be, the conception and study of semantics-preserving program transformations that can be used in a compiler to optimize for execution speed. This thesis reports on our furthering of that kind of applications (Chapters 6-9), but also on somewhat surprising applications outside the core area of programming language research as such (Chapters 4 and 5). Another topic that is covered is a series of investigations into the theoretical underpinning of free theorems as regards aspects of Haskell previously unaccounted for (Chapters 8 and 10). To set the stage, though, Chapters 2 and 3 first give a brief introduction to Haskell, its abstraction facilities and associated reasoning techniques in general and on the type level, and a program transformation technique of the mentioned kind. The subsequent chapters then provide high-level overviews of the results obtained in the full papers that are appended after page 84." tags: - "control systems" - "programming languages" - "optimization" - "semantics" - "reusable components" - "rule-based" - "transformation engineering" - "Java" - "program analysis" - "software components" - "program verification" - "formal semantics" - "language engineering" - "transformation language" - "software language engineering" - "functional programming" - "design research" - "software component" - "analysis" - "language design" - "static analysis" - "Haskell" - "type system" - "reuse" - "equational proofs" - "software engineering" - "rules" - "algebraic specification" - "C++" - "programming paradigms" - "type checking" - "transformation system" - "compiler" - " algebra" - "programming" - "context-aware" - "abstraction" - "program optimization" - "design" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi08e" cites: 0 citedby: 0 kind: "misc" key: "Voi08e" - title: "Deaccumulation - Improving Provability" author: - name: "Jürgen Giesl" link: "http://verify.rwth-aachen.de/giesl/" - name: "Armin Kühnemann" link: "http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/k/K=uuml=hnemann:Armin.html" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2896&spage=146" abstract: "Several induction theorem provers were developed to verify functional programs mechanically. Unfortunately, automated verification usually fails for functions with accumulating arguments. In particular, this holds for tail-recursive functions that correspond to imperative programs, but also for programs with nested recursion. Based on results from the theory of tree transducers, we develop an automatic transformation technique. It transforms accumulative functional programs into non-accumulative ones, which are much better suited for automated verification by induction theorem provers. Hence, in contrast to classical program transformations aiming at improving the efficiency, the goal of our deaccumulation technique is to improve the provability." links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2896&spage=146" successor: "https://researchr.org/publication/GKV07" tags: - "rule-based" - "program verification" - "functional programming" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/GKV03" cites: 0 citedby: 0 pages: "146-160" booktitle: "asian" kind: "inproceedings" key: "GKV03" - title: "Using circular programs to deforest in accumulating parameters" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2002" doi: "http://doi.acm.org/10.1145/568173.568187" abstract: "Functional languages allow a modular programming style by function composition, which however can lead to inefficient runtime behavior due to production and consumption of intermediate results. We present a new mechanizable transformation technique for removing intermediate data structures in the composition of two functions from a class of recursive functions with accumulating parameters, for which classical deforestation techniques fail. In order to avoid multiple traversals of the input data structure, the composition algorithm produces circular programs that make essential use of lazy evaluation and local recursion. The resulting programs are simplified using a post-processing phase presented in the paper." links: doi: "http://doi.acm.org/10.1145/568173.568187" successor: "https://researchr.org/publication/Voi04a" tags: - "laziness" - "programming languages" - "data-flow language" - "traversal" - "transformation language" - "composition" - "functional programming" - "data-flow programming" - "data-flow" - "programming" - "higher-order transformations" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Voi02b" cites: 0 citedby: 0 pages: "126-137" booktitle: "PEPM" kind: "inproceedings" key: "Voi02b" - title: "Tree Transducer Composition as Program Transformation" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2005" abstract: "Nonstrict, purely functional programming languages offer a high potential for the modularization of software. But beside their advantages with respect to reliability and reusability, modularly specified programs often have the disadvantage of low execution efficiency, caused in particular by the creation and consumption of structured intermediate results. One possible approach to cure this conflict is the automatic, semantics-preserving optimization of programs, for which purely functional languages are again particularly suited due to their mathematical foundation. This dissertation studies a specific transformation for the elimination of intermediate results (for so called deforestation) regarding its impact on the program efficiency under nonstrict evaluation. The formal framework is provided by concepts from the theory of tree transducers. One special feature of the transformation under consideration is the successful handling of accumulating parameters, which find frequent use in functional programs. The core of the thesis is the derivation of effectively decidable, syntactic conditions on the original program under which the transformed program is to be preferred over it with respect to efficiency." tags: - "programming languages" - "optimization" - "object-oriented programming" - "semantics" - "formal semantics" - "transformation language" - "composition" - "functional programming" - "reuse" - "programming" - "subject-oriented programming" - "program optimization" - "reliability" - "systematic-approach" - "feature-oriented programming" - "transformation" - "program transformation" - "domain-specific language" researchr: "https://researchr.org/publication/Voi05" cites: 0 citedby: 0 school: "Technische Universität Dresden" advisor: - name: "Armin Kühnemann" link: "http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/k/K=uuml=hnemann:Armin.html" - name: "Heiko Vogler" link: "http://www.inf.tu-dresden.de/index.php?node_id=1568&ln=en" kind: "phdthesis" key: "Voi05" - title: "6. Arbeitstagung Programmiersprachen (ATPS 2013)" author: - name: "Jens Knoop" link: "http://www.complang.tuwien.ac.at/knoop/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2013" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/se/KnoopV13" researchr: "https://researchr.org/publication/KnoopV13" cites: 0 citedby: 0 pages: "369" booktitle: "se" kind: "inproceedings" key: "KnoopV13" - title: "Proceedings of the ACM SIGPLAN 2010 Workshop on Partial Evaluation and Program Manipulation" year: "2010" month: "January" links: "website": "http://www.program-transformation.org/PEPM10" tags: - "partial evaluation" researchr: "https://researchr.org/publication/pepm%3A2010" cites: 0 citedby: 0 booktitle: "Proceedings of the ACM SIGPLAN 2010 Workshop on Partial Evaluation and Program Manipulation" conference: "PEPM" editor: - name: "John P. Gallagher" link: "http://akira.ruc.dk/~jpg/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" publisher: "ACM" kind: "proceedings" key: "pepm:2010" - title: "Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012, Copenhagen, Denmark, 13 September 2012" year: "2012" doi: "http://dl.acm.org/citation.cfm?id=2364506" links: doi: "http://dl.acm.org/citation.cfm?id=2364506" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/2012" researchr: "https://researchr.org/publication/haskell-2012" cites: 0 citedby: 0 booktitle: "Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012, Copenhagen, Denmark, 13 September 2012" conference: "haskell" editor: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" publisher: "ACM" isbn: "978-1-4503-1574-6" kind: "proceedings" key: "haskell-2012"