Publications: (@DBLP, @ACM DL, @Google Scholar)

Book chapter:

• N. Foster, K. Matsuda, and J. Voigtländer
  Three Complementary Approaches to Bidirectional Programming (bib)
  In Spring School on Generic and Indexed Programming (SSGIP'10), Oxford, England, Revised Lectures, volume 7470 of LNCS, pages 1-46, Springer, 2012.

Journals:

• H. Grohne and J. Voigtländer
  Formalizing Semantic Bidirectionalization and Extensions with Dependent Types (bib)
  Journal of Logical and Algebraic Methods in Programming, volume 86(1), pages 319-348, Elsevier, 2017.
• J. Voigtländer, Z. Hu, K. Matsuda, and M. Wang
  Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins (bib)
  Journal of Functional Programming, volume 23(5), pages 515-551, Cambridge University Press, 2013.
• D. Seidel and J. Voigtländer
  Refined Typing to Localize the Impact of Forced Strictness on Free Theorems (bib)
  Acta Informatica, volume 48(3), pages 191-211, Springer, 2011.
  The implementation of the algorithm developed in this paper is accessible via a web interface here.
• P. Johann and J. Voigtländer
  A family of syntactic logical relations for the semantics of Haskell-like languages (bib)
  Information and Computation, volume 207(2), pages 341-368, Elsevier, 2009.
• J. Voigtländer and P. Johann
  Selective strictness and parametricity in structural operational semantics, inequationally (bib)
  Theoretical Computer Science, volume 388(1-3), pages 290-318, Elsevier, 2007.
• J. Voigtländer
  Formal Efficiency Analysis for Tree Transducer Composition (bib)
  Theory of Computing Systems, volume 41(4), pages 619-689, Springer, 2007.
• J. Giesl, A. Kühnemann, and J. Voigtländer
  Deaccumulation techniques for improving provability (bib)
  Journal of Logic and Algebraic Programming, volume 71(2), pages 79-113, Elsevier, 2007.
• P. Johann and J. Voigtländer
  The Impact of seq on Free Theorems-Based Program Transformations (bib)
  Fundamenta Informaticae, volume 69(1-2), pages 63-102, IOS Press, 2006.
• J. Voigtländer and A. Kühnemann
  Composition of functions with accumulating parameters (bib)
  Journal of Functional Programming, volume 14(3), pages 317-363, Cambridge University Press, 2004.
  The proof appendix is available online.
• J. Voigtländer
  Using Circular Programs to Deforest in Accumulating Parameters (bib)
  Higher-Order and Symbolic Computation, volume 17(1-2), pages 129-163, Kluwer, 2004.

Proceedings:

• T. Gödderz and J. Voigtländer
  Automatic Testing of Operation Invariance (bib)
  In 23rd International Workshop on Functional and (Constraint) Logic Programming (WFLP'14), Wittenberg, Germany, Proceedings, pages 172-186, volume 1335 of CEUR Workshop Proceedings, September 2014.
  An implementation of the approach discussed in this paper is available here.
• S. Mehner, D. Seidel, L. Straßburger, and J. Voigtländer
  Parametricity and Proving Free Theorems for Functional-Logic Languages (bib)
  In 16th International Symposium on Principles and Practice of Declarative Programming (PPDP'14, acceptance rate 22/43), Canterbury, UK, Proceedings, pages 19-30, ACM, September 2014.
  The paper is available via the ACM DL Author-ize feature here.
• H. Grohne, A. Löh, and J. Voigtländer
  Formalizing Semantic Bidirectionalization with Dependent Types (bib)
  In Third International Workshop on Bidirectional Transformations (BX'14, acceptance rate 9/17), an EDBT/ICDT workshop, Athens, Greece, Proceedings, pages 75-81, volume 1133 of CEUR Workshop Proceedings, March 2014.
• R. Bird, J. Gibbons, S. Mehner, T. Schrijvers, and J. Voigtländer
  Understanding Idiomatic Traversals Backwards and Forwards (bib)
  In Haskell Symposium 2013 (Haskell'13, acceptance rate 13/33), Boston, Massachusetts, Proceedings, pages 25-36, ACM, September 2013.
  The paper is available via the ACM DL Author-ize feature here.
• J. Voigtländer
  Ideas for Connecting Inductive Program Synthesis and Bidirectionalization (bib)
  In Workshop on Partial Evaluation and Program Manipulation (PEPM'12, acceptance rate 19/37), Philadelphia, Pennsylvania, Proceedings, pages 39-42, ACM, January 2012.
  The paper is available via the ACM DL Author-ize feature here.
• D. Seidel and J. Voigtländer
  Improvements for Free (bib)
  In 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11, acceptance rate 11/13), Saarbrücken, Germany, Post-Proceedings, volume 57 of EPTCS, pages 89-103, 2011.
• J.P. Fernandes, J. Saraiva, D. Seidel, and J. Voigtländer
  Strictification of Circular Programs (bib)
  In Workshop on Partial Evaluation and Program Manipulation (PEPM'11, acceptance rate 15/35), Austin, Texas, Proceedings, pages 131-140, ACM, January 2011.
  The paper is available via the ACM DL Author-ize feature here.
• J. Voigtländer, Z. Hu, K. Matsuda, and M. Wang
  Combining Syntactic and Semantic Bidirectionalization (bib)
  In 15th International Conference on Functional Programming (ICFP'10, acceptance rate 33/99), Baltimore, Maryland, Proceedings, volume 45(9) of SIGPLAN Notices, pages 181-192, ACM, September 2010.
  The paper is available via the ACM DL Author-ize feature here.
  A web interface to the methods discussed in this paper is accessible here.
  A video of the conference presentation is available here.
• P. Johann, A. Simpson, and J. Voigtländer
  A Generic Operational Metatheory for Algebraic Effects (bib)
  In 25th Symposium on Logic in Computer Science (LICS'10, acceptance rate 40/149), Edinburgh, Scotland, Proceedings, pages 209-218, IEEE, July 2010.
• D. Seidel and J. Voigtländer
  Proving Properties About Functions on Lists Involving Element Tests (bib)
  In 20th International Workshop on Algebraic Development Techniques (WADT'10), Schloss Etelsen, Germany, Revised Selected Papers (acceptance rate 15/32), volume 7137 of LNCS, pages 270-286, Springer, February 2012.
• D. Seidel and J. Voigtländer
  Automatically Generating Counterexamples to Naive Free Theorems (bib)
  In 10th International Symposium on Functional and Logic Programming (FLOPS'10, acceptance rate 21/49), Sendai, Japan, Proceedings, volume 6009 of LNCS, pages 175-190, Springer, April 2010.
  The implementation of the algorithm presented in this paper is accessible via a web interface here.
• J. Christiansen, D. Seidel, and J. Voigtländer
  Free Theorems for Functional Logic Programs (bib)
  In 4th Workshop on Programming Languages meets Program Verification (PLPV'10, acceptance rate 7/10), Madrid, Spain, Proceedings, pages 39-48, ACM, January 2010.
  The paper is available via the ACM DL Author-ize feature here.
• J. Christiansen, D. Seidel, and J. Voigtländer
  An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry (bib)
  In 19th International Workshop on Functional and (Constraint) Logic Programming (WFLP'10, acceptance rate 12/15), Madrid, Spain, Revised Selected Papers (acceptance rate 8/12), volume 6559 of LNCS, pages 119-136, Springer, 2011.
  We found that two of the conjectures in the paper do not hold, see the online appendix for details. There is also a revised version available as a technical report, incorporating the corrections, see below.
• D. Seidel and J. Voigtländer
  Taming Selective Strictness (bib)
  In 4. Arbeitstagung Programmiersprachen (ATPS'09, acceptance rate 8/11) der GI-Fachgruppe "Programmiersprachen und Rechenkonzepte" im Rahmen der GI-Jahrestagung Informatik 2009, Lübeck, Germany, Proceedings, volume 154 of Lecture Notes in Informatics, pages 2916-2930, GI, October 2009.
  An extended version of this work appeared in Acta Informatica, see above.
• J. Voigtländer
  Free Theorems Involving Type Constructor Classes (bib)
  In 14th International Conference on Functional Programming (ICFP'09, acceptance rate 32/101), Edinburgh, Scotland, Proceedings, volume 44(9) of SIGPLAN Notices, pages 173-184, ACM, September 2009.
  The paper is available via the ACM DL Author-ize feature here.
  A video of the conference presentation is available here.
• F. Stenger and J. Voigtländer
  Parametricity for Haskell with Imprecise Error Semantics (bib)
  In 9th International Conference on Typed Lambda Calculi and Applications (TLCA'09, acceptance rate 27/53), Brasília, Brazil, Proceedings, volume 5608 of LNCS, pages 294-308, Springer, July 2009.
• J. Voigtländer
  Bidirectionalization for Free! (bib)
  In 36th Symposium on Principles of Programming Languages (POPL'09, acceptance rate 36/160), Savannah, Georgia, Proceedings, volume 44(1) of SIGPLAN Notices, pages 165-176, ACM, January 2009.
  The paper is available via the ACM DL Author-ize feature here.
  A web interface to the library developed in this paper is now accessible here. (The links mentioned in the paper itself are outdated.)
• J. Voigtländer
  Asymptotic Improvement of Computations over Free Monads (bib)
  In 9th International Conference on Mathematics of Program Construction (MPC'08, acceptance rate 18/41), Marseille, France, Proceedings, volume 5133 of LNCS, pages 388-403, Springer, July 2008.
• J. Voigtländer
  Semantics and Pragmatics of New Shortcut Fusion Rules (bib)
  In 9th International Symposium on Functional and Logic Programming (FLOPS'08, acceptance rate 20/59), Ise, Japan, Proceedings, volume 4989 of LNCS, pages 163-179, Springer, April 2008.
• J. Voigtländer
  Much Ado about Two: A Pearl on Parallel Prefix Computation (bib)
  In 35th Symposium on Principles of Programming Languages (POPL'08, acceptance rate 35/212), San Francisco, California, Proceedings, volume 43(1) of SIGPLAN Notices, pages 29-35, ACM, January 2008.
  The paper is available via the ACM DL Author-ize feature here.
• J. Voigtländer
  Proving Correctness via Free Theorems: The Case of the destroy/build-Rule (bib)
  In Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'08, acceptance rate 20/74), San Francisco, California, Proceedings, pages 13-20, ACM, January 2008.
  The paper is available via the ACM DL Author-ize feature here.
  The tool used in this paper to derive free theorems is now accessible via a web interface here. (The paper itself mentions an older link.)
• P. Johann and J. Voigtländer
  Free Theorems in the Presence of seq (bib)
  In 31st Symposium on Principles of Programming Languages (POPL'04, acceptance rate 29/176), Venice, Italy, Proceedings, volume 39(1) of SIGPLAN Notices, pages 99-110, ACM, January 2004.
  The paper is available via the ACM DL Author-ize feature here.
  An extended version of this work appeared in Fundamenta Informaticae, see above.
• J. Giesl, A. Kühnemann, and J. Voigtländer
  Deaccumulation - Improving Provability (bib)
  In 8th Asian Computing Science Conference (ASIAN'03, acceptance rate 16/53), Mumbai, India, Proceedings, volume 2896 of LNCS, pages 146-160, Springer, December 2003.
  An extended version of this work appeared in Journal of Logic and Algebraic Programming, see above.
• J. Voigtländer
  Concatenate, Reverse and Map Vanish For Free (bib)
  In 7th International Conference on Functional Programming (ICFP'02, acceptance rate 24/76), Pittsburgh, Pennsylvania, Proceedings, volume 37(9) of SIGPLAN Notices, pages 14-25, ACM, October 2002.
  The paper is available via the ACM DL Author-ize feature here.
• J. Voigtländer
  Using Circular Programs to Deforest in Accumulating Parameters (bib)
  In Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM'02, acceptance rate 11/21), Aizu, Japan, Proceedings, pages 126-137, ACM, September 2002.
  An extended version of this work appeared in Higher-Order and Symbolic Computation, see above.
• J. Voigtländer
  Conditions for Efficiency Improvement by Tree Transducer Composition (bib)
  In 13th International Conference on Rewriting Techniques and Applications (RTA'02, acceptance rate 20/40), Copenhagen, Denmark, Proceedings, volume 2378 of LNCS, pages 222-236, Springer, July 2002.

Theses:

• J. Voigtländer
  Types for Programming and Reasoning
  Habilitation thesis, Technische Universität Dresden, defended in July 2009.
• J. Voigtländer
  Tree Transducer Composition as Program Transformation (bib)
  PhD thesis, Technische Universität Dresden, defended in January 2005.
  This thesis is also available as a book.
• J. Voigtländer
  Composition of restricted Macro Tree Transducers (bib)
  Master thesis, Technische Universität Dresden, defended in April 2001.
  An article based on this thesis appeared in Journal of Functional Programming, see above.

Technical Reports:

• H. Pacheco, N. Macedo, A. Cunha, and J. Voigtländer
  A Generic Scheme and Properties of Bidirectional Transformations (bib)
  arXiv:1306.4473
• J. Christiansen, D. Seidel, and J. Voigtländer
  An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry without Letrec (bib)
  Technical Report IAI-TR-2011-1, University of Bonn, March 2011.
• D. Seidel and J. Voigtländer
  Taming Selective Strictness (bib)
  Technical Report TUD-FI09-06, Technische Universität Dresden, June 2009.
  A revised version of this work appeared in Acta Informatica, see above.
• F. Stenger and J. Voigtländer
  Parametricity for Haskell with Imprecise Error Semantics (bib)
  Technical Report TUD-FI08-08, Technische Universität Dresden, November 2008.
  An abridged version of this work appeared at TLCA'09, see above.
• J. Voigtländer and P. Johann
  Selective Strictness and Parametricity in Structural Operational Semantics (bib)
  Technical Report TUD-FI06-02, Technische Universität Dresden, June 2006.
  A revised version of this work appeared in Theoretical Computer Science, see above.
• J. Giesl, A. Kühnemann, and J. Voigtländer
  Deaccumulation Techniques for Improving Provability (bib)
  Technical Report TUD-FI05-14, Technische Universität Dresden, December 2005.
  A slightly revised version of this work appeared in Journal of Logic and Algebraic Programming, see above.
• J. Voigtländer
  Formal Efficiency Analysis for Tree Transducer Composition (bib)
  Technical Report TUD-FI04-08, Technische Universität Dresden, June 2004.
  An abridged and revised version of this work appeared in Theory of Computing Systems, see above.
• J. Voigtländer and A. Kühnemann
  Composition of Functions with Accumulating Parameters (bib)
  Technical Report TUD-FI01-08, Technische Universität Dresden, August 2001.
  A much revised version of this work appeared in Journal of Functional Programming, see above.
• A. Kühnemann and J. Voigtländer
  Tree Transducer Composition as Deforestation Method for Functional Programs (bib)
  Technical Report TUD-FI01-07, Technische Universität Dresden, August 2001.