publications: - 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: "Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings" editor: - name: "Matthias Blume" link: "https://researchr.org/alias/matthias-blume" - name: "Naoki Kobayashi" link: "https://researchr.org/alias/naoki-kobayashi" - name: "Germán Vidal" link: "https://researchr.org/alias/germ%C3%A1n-vidal" volume: "6009" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-12250-7" kind: "inproceedings" key: "SV10" - 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: "Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, Austin, TX, USA, January 24-25, 2011" editor: - name: "Siau-Cheng Khoo" link: "https://researchr.org/alias/siau-cheng-khoo" - name: "Jeremy G. Siek" link: "http://homes.soic.indiana.edu/jsiek/" publisher: "ACM" isbn: "978-1-4503-0485-6" kind: "inproceedings" key: "FernandesSSV11" - title: "A semantics for weakly encapsulated search in functional logic programs" author: - name: "Jan Christiansen" link: "http://korsika.informatik.uni-kiel.de/~jac/wordpress/" - name: "Michael Hanus" link: "https://researchr.org/alias/michael-hanus" - name: "Fabian Reck" link: "https://researchr.org/alias/fabian-reck" - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" year: "2013" doi: "http://doi.acm.org/10.1145/2505879.2505896" links: doi: "http://doi.acm.org/10.1145/2505879.2505896" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/ChristiansenHRS13" researchr: "https://researchr.org/publication/ChristiansenHRS13" cites: 0 citedby: 0 pages: "49-60" booktitle: "15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013" editor: - name: "Ricardo Peña" link: "https://researchr.org/alias/ricardo-pe%C3%B1a" - name: "Tom Schrijvers" link: "https://researchr.org/alias/tom-schrijvers" publisher: "ACM" isbn: "978-1-4503-2154-9" kind: "inproceedings" key: "ChristiansenHRS13" - title: "Countable homogeneous multipartite graphs" author: - name: "Tristan Jenkinson" link: "https://researchr.org/alias/tristan-jenkinson" - name: "J. K. Truss" link: "https://researchr.org/alias/j.-k.-truss" - name: "Daniel Seidel" link: "http://wob.iai.uni-bonn.de/Wob/en/view/class217_id1454.html" year: "2012" doi: "http://dx.doi.org/10.1016/j.ejc.2011.04.004" links: doi: "http://dx.doi.org/10.1016/j.ejc.2011.04.004" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/ejc/JenkinsonTS12" researchr: "https://researchr.org/publication/JenkinsonTS12" cites: 0 citedby: 0 journal: "Eur. J. Comb." volume: "33" number: "1" pages: "82-109" kind: "article" key: "JenkinsonTS12" - 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 Notices" volume: "44" number: "11" pages: "7" kind: "article" key: "ChristiansenSV09" - 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: "Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010" editor: - name: "Cormac Flanagan" link: "https://researchr.org/alias/cormac-flanagan" - name: "Jean-Christophe Filliâtre" link: "https://researchr.org/alias/jean-christophe-filli%C3%A2tre" publisher: "ACM" isbn: "978-1-60558-890-2" kind: "inproceedings" key: "CSV10" - 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: "Informatik 2009: Im Focus das Leben, Beiträge der 39. Jahrestagung der Gesellschaft für Informatik e.V. (GI), 28.9.-2.10.2009, Lübeck, Proceedings" editor: - name: "Stefan Fischer" link: "https://researchr.org/alias/stefan-fischer" - name: "Erik Maehle" link: "https://researchr.org/alias/erik-maehle" - name: "Rüdiger Reischuk" link: "https://researchr.org/alias/r%C3%BCdiger-reischuk" volume: "154" series: "LNI" publisher: "GI" isbn: "978-3-88579-248-2" kind: "inproceedings" key: "SV09" - 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 Informatica" volume: "48" number: "3" pages: "191-211" kind: "article" key: "SeidelV11" - 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: "Functional and Constraint Logic Programming - 19th International Workshop, WFLP 2010, Madrid, Spain, January 17, 2010. Revised Selected Papers" editor: - name: "Julio Mariño" link: "https://researchr.org/alias/julio-mari%C3%B1o" volume: "6559" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-20774-7" kind: "inproceedings" key: "ChristiansenSV10" - title: "Minimally strict polymorphic functions" 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" year: "2011" doi: "http://doi.acm.org/10.1145/2003476.2003487" links: doi: "http://doi.acm.org/10.1145/2003476.2003487" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/ChristiansenS11" researchr: "https://researchr.org/publication/ChristiansenS11" cites: 0 citedby: 0 pages: "53-64" booktitle: "Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark" editor: - name: "Peter Schneider-Kamp" link: "https://researchr.org/alias/peter-schneider-kamp" - name: "Michael Hanus" link: "https://researchr.org/alias/michael-hanus" publisher: "ACM" isbn: "978-1-4503-0776-5" kind: "inproceedings" key: "ChristiansenS11" - 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: "Recent Trends in Algebraic Development Techniques - 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers" editor: - name: "Till Mossakowski" link: "https://researchr.org/alias/till-mossakowski" - name: "Hans-Jörg Kreowski" link: "https://researchr.org/alias/hans-j%C3%B6rg-kreowski" volume: "7137" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-28411-3" kind: "inproceedings" key: "SeidelV10"