@mastersthesis{jansson1995polytypism, title = {Polytypism and polytypic unification}, author = {Jansson, Patrik}, school = {Chalmers University of Technology, Sweden}, year = 1995 } @inproceedings{DBLP:conf/afp/JeuringJ96, author = {Johan Jeuring and Patrik Jansson}, editor = {John Launchbury and Erik Meijer and Tim Sheard}, title = {Polytypic Programming}, booktitle = {Advanced Functional Programming, Second International School, Olympia, WA, USA, August 26-30, 1996, Tutorial Text}, shortbooktitle ={Advanced Functional Programming}, series = {Lecture Notes in Computer Science}, volume = 1129, pages = {68--114}, publisher = {Springer}, year = 1996, COMMENTurl = {https://doi.org/10.1007/3-540-61628-4_3}, doi = {10.1007/3-540-61628-4_3}, timestamp = {Tue, 14 May 2019 10:00:44 +0200}, biburl = {https://dblp.org/rec/conf/afp/JeuringJ96.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/popl/JanssonJ97, author = {Patrik Jansson and Johan Jeuring}, editor = {Peter Lee and Fritz Henglein and Neil D. Jones}, title = {{PolyP} - {A} Polytypic Programming Language}, booktitle = {Conference Record of {POPL}'97: The 24th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997}, shortbooktitle ={{POPL}'97}, pages = {470--482}, publisher = {{ACM} Press}, ISBN = 0897918533, year = 1997, COMMENTurl = {https://doi.org/10.1145/263699.263763}, doi = {10.1145/263699.263763}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/popl/JanssonJ97.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @book{jansson1997functional, title = {Functional polytypic programming use and implementation}, author = {Jansson, Patrik}, year = 1997, publisher = {Department of Computing Science, Chalmers University of Technology, Sweden}, ISBN = 9171974865, note = {Licentiate thesis} } @inproceedings{jansson1998polylib, title = {PolyLib—A library of polytypic functions}, author = {Jansson, Patrik and Jeuring, Johan}, booktitle = {Workshop on generic programming, WGP'98}, year = 1998, url = "http://www.cse.chalmers.se/~patrikj/poly/polylib/polylib.ps.gz" } @article{DBLP:journals/jfp/JanssonJ98, author = {Patrik Jansson and Johan Jeuring}, title = {Polytypic Unification}, journal = {J. Funct. Program.}, volume = 8, number = 5, pages = {527--536}, year = 1998, doi = {10.1017/S095679689800313X}, publisher = {Cambridge University Press}, url = {http://journals.cambridge.org/action/displayAbstract?aid=44195}, timestamp = {Fri, 10 Jun 2011 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/JanssonJ98.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/afp/BackhouseJJM98, author = {Roland Carl Backhouse and Patrik Jansson and Johan Jeuring and Lambert G. L. T. Meertens}, editor = {S. Doaitse Swierstra and Pedro Rangel Henriques and Jos{\'{e}} Nuno Oliveira}, title = {Generic Programming: An Introduction}, shortbooktitle={Advanced Functional Programming}, booktitle = {Advanced Functional Programming, Third International School, Braga, Portugal, September 12-19, 1998, Revised Lectures}, series = {Lecture Notes in Computer Science}, volume = 1608, pages = {28--115}, publisher = {Springer}, year = 1998, COMMENTurl = {https://doi.org/10.1007/10704973_2}, doi = {10.1007/10704973_2}, timestamp = {Tue, 14 May 2019 10:00:44 +0200}, biburl = {https://dblp.org/rec/conf/afp/BackhouseJJM98.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/esop/JanssonJ99, author = {Patrik Jansson and Johan Jeuring}, editor = {S. Doaitse Swierstra}, title = {Polytypic Compact Printing and Parsing}, booktitle = {Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, 22-28 March, 1999, Proceedings}, shortbooktitle ={European Symposium on Programming, {ESOP}'99}, series = {Lecture Notes in Computer Science}, volume = 1576, pages = {273--287}, publisher = {Springer}, year = 1999, COMMENTurl = {https://doi.org/10.1007/3-540-49099-X_18}, doi = {10.1007/3-540-49099-X_18}, timestamp = {Tue, 14 May 2019 10:00:41 +0200}, biburl = {https://dblp.org/rec/conf/esop/JanssonJ99.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @phdthesis{DBLP:phd/basesearch/Jansson00, author = {Patrik Jansson}, title = {Functional Polytypic Programming}, number = 1548, school = {Chalmers University of Technology, Gothenburg, Sweden}, year = 2000, url = {http://publications.lib.chalmers.se/publication/804-functional-polytypic-programming}, ISBN = {917197895X}, timestamp = {Mon, 13 Mar 2017 00:00:00 +0100}, biburl = {https://dblp.org/rec/phd/basesearch/Jansson00.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{jansson2000framework, title = {A Framework for Polytypic Programming on Terms, with an Application to Rewriting}, author = {Jansson, Patrik and Jeuring, Johan}, booktitle = {Proceedings Workshop on Generic Programming (WGP2000), Ponte de Lima, Portugal}, year = 2000, url = "https://webspace.science.uu.nl/~jeuri101/homepage/Publications/terminterface.pdf" } @article{DBLP:journals/scp/JanssonJ02, author = {Patrik Jansson and Johan Jeuring}, title = {Polytypic data conversion programs}, journal = {Sci. Comput. Program.}, volume = 43, number = 1, pages = {35--75}, year = 2002, publisher = {Elsevier}, COMMENTurl = {https://doi.org/10.1016/S0167-6423(01)00020-X}, doi = {10.1016/S0167-6423(01)00020-X}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/scp/JanssonJ02.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/ifl/NorellJ03, author = {Ulf Norell and Patrik Jansson}, editor = {Philip W. Trinder and Greg Michaelson and Ricardo Pena}, title = {Polytypic Programming in {Haskell}}, booktitle = {Implementation of Functional Languages, 15th International Workshop, {IFL} 2003, Edinburgh, UK, September 8-11, 2003, Revised Papers}, shortbooktitle ={Implementation of Functional Languages}, series = {Lecture Notes in Computer Science}, volume = 3145, pages = {168--184}, publisher = {Springer}, year = 2003, COMMENTurl = {https://doi.org/10.1007/978-3-540-27861-0_11}, doi = {10.1007/978-3-540-27861-0_11}, timestamp = {Tue, 14 May 2019 10:00:35 +0200}, biburl = {https://dblp.org/rec/conf/ifl/NorellJ03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/njc/BenkeDJ03, author = {Marcin Benke and Peter Dybjer and Patrik Jansson}, title = {Universes for Generic Programs and Proofs in Dependent Type Theory}, journal = {Nord. J. Comput.}, volume = 10, number = 4, pages = {265--289}, year = 2003, timestamp = {Wed, 14 Jan 2004 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/njc/BenkeDJ03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/mpc/DanielssonJ04, author = {Nils Anders Danielsson and Patrik Jansson}, editor = {Dexter Kozen and Carron Shankland}, title = {Chasing Bottoms: {A} Case Study in Program Verification in the Presence of Partial and Infinite Values}, booktitle = {Mathematics of Program Construction, 7th International Conference, {MPC} 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings}, shortbooktitle ={Mathematics of Program Construction}, series = {Lecture Notes in Computer Science}, ISBN = 3540223800, volume = 3125, pages = {85--109}, publisher = {Springer}, year = 2004, COMMENTurl = {https://doi.org/10.1007/978-3-540-27764-4_6}, doi = {10.1007/978-3-540-27764-4_6}, timestamp = {Tue, 14 May 2019 10:00:46 +0200}, biburl = {https://dblp.org/rec/conf/mpc/DanielssonJ04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/mpc/NorellJ04, author = {Ulf Norell and Patrik Jansson}, editor = {Dexter Kozen and Carron Shankland}, title = {Prototyping Generic Programming in {Template} {Haskell}}, booktitle = {Mathematics of Program Construction, 7th International Conference, {MPC} 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings}, series = {Lecture Notes in Computer Science}, volume = 3125, pages = {314--333}, publisher = {Springer}, year = 2004, COMMENTurl = {https://doi.org/10.1007/978-3-540-27764-4_17}, doi = {10.1007/978-3-540-27764-4_17}, ISBN = 3540223800, timestamp = {Sun, 04 Jun 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/mpc/NorellJ04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/popl/DanielssonHJG06, author = {Nils Anders Danielsson and John Hughes and Patrik Jansson and Jeremy Gibbons}, editor = {J. Gregory Morrisett and Simon L. Peyton Jones}, title = {Fast and loose reasoning is morally correct}, booktitle = {Proceedings of the 33rd {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2006, Charleston, South Carolina, USA, January 11-13, 2006}, pages = {206--217}, publisher = {{ACM}}, ISBN = 1595930272, year = 2006, COMMENTurl = {https://doi.org/10.1145/1111037.1111056}, doi = {10.1145/1111037.1111056}, timestamp = {Sun, 25 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/popl/DanielssonHJG06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/ifl/JanssonJCEKMOV06, author = {Patrik Jansson and Johan Jeuring and Laurence Cabenda and Gerbo Engels and Jacob Kleerekoper and Sander Mak and Michiel Overeem and Kees Visser}, editor = {Zolt{\'{a}}n Horv{\'{a}}th and Vikt{\'{o}}ria Zs{\'{o}}k and Andrew Butterfield}, title = {Testing Properties of Generic Functions}, booktitle = {Implementation and Application of Functional Languages, 18th International Symposium, {IFL} 2006, Budapest, Hungary, September 4-6, 2006, Revised Selected Papers}, shortbooktitle ={Symposium on Implementation and Application of Functional Languages}, series = {Lecture Notes in Computer Science}, volume = 4449, pages = {217--234}, publisher = {Springer}, year = 2006, COMMENTurl = {https://doi.org/10.1007/978-3-540-74130-5_13}, doi = {10.1007/978-3-540-74130-5_13}, timestamp = {Tue, 14 May 2019 10:00:35 +0200}, biburl = {https://dblp.org/rec/conf/ifl/JanssonJCEKMOV06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/mpc/MuKJ08, author = {Shin{-}Cheng Mu and Hsiang{-}Shang Ko and Patrik Jansson}, editor = {Philippe Audebaud and Christine Paulin{-}Mohring}, title = {Algebra of Programming Using Dependent Types}, booktitle = {Mathematics of Program Construction, 9th International Conference, {MPC} 2008, Marseille, France, July 15-18, 2008. Proceedings}, shortbooktitle ={International Conference on Mathematics of Program Construction}, series = {Lecture Notes in Computer Science}, volume = 5133, pages = {268--283}, publisher = {Springer}, year = 2008, COMMENTurl = {https://doi.org/10.1007/978-3-540-70594-9_15}, doi = {10.1007/978-3-540-70594-9_15}, timestamp = {Fri, 27 Mar 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/mpc/MuKJ08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/icfp/BernardyJZSP08, author = {Jean{-}Philippe Bernardy and Patrik Jansson and Marcin Zalewski and Sibylle Schupp and Andreas P. Priesnitz}, editor = {Ralf Hinze and Don Syme}, title = {A comparison of {C++} concepts and {Haskell} type classes}, booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Generic Programming, {WGP} 2008, Victoria, BC, Canada, September 20, 2008}, pages = {37--48}, publisher = {{ACM}}, year = 2008, COMMENTurl = {https://doi.org/10.1145/1411318.1411324}, doi = {10.1145/1411318.1411324}, timestamp = {Tue, 06 Nov 2018 16:59:25 +0100}, biburl = {https://dblp.org/rec/conf/icfp/BernardyJZSP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/icfp/2009wgp, editor = {Patrik Jansson and Sibylle Schupp}, title = {Proceedings of the 2009 {ACM} {SIGPLAN} workshop on Generic programming, WGP@ICFP 2009, Edinburgh, United Kingdom, August 31 - September 2, 2009}, publisher = {{ACM}}, year = 2009, COMMENTurl = {https://doi.org/10.1145/1596614}, doi = {10.1145/1596614}, isbn = {978-1-60558-510-9}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/icfp/2009wgp.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/haskell/RodriguezJJGKO08, author = {Alexey Rodriguez and Johan Jeuring and Patrik Jansson and Alex Gerdes and Oleg Kiselyov and Bruno C. d. S. Oliveira}, editor = {Andy Gill}, title = {Comparing libraries for generic programming in haskell}, booktitle = {Proceedings of the 1st {ACM} {SIGPLAN} Symposium on {Haskell}, {Haskell} 2008, Victoria, BC, Canada, 25 September 2008}, pages = {111--122}, publisher = {{ACM}}, year = 2008, COMMENTurl = {https://doi.org/10.1145/1411286.1411301}, doi = {10.1145/1411286.1411301}, ISBN = 9781605580647, timestamp = {Fri, 25 Jun 2021 14:48:54 +0200}, biburl = {https://dblp.org/rec/conf/haskell/RodriguezJJGKO08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/dsl/LinckeJZI09, author = {Daniel Lincke and Patrik Jansson and Marcin Zalewski and Cezar Ionescu}, editor = {Walid Mohamed Taha}, title = {Generic Libraries in {C++} with Concepts from High-Level Domain Descriptions in {Haskell}}, booktitle = {Domain-Specific Languages, {IFIP} {TC} 2 Working Conference, {DSL} 2009, Oxford, UK, July 15-17, 2009, Proceedings}, shortbooktitle ={{IFIP} Working Conference on Domain-Specific Languages}, series = {Lecture Notes in Computer Science}, volume = 5658, pages = {236--261}, publisher = {Springer}, year = 2009, COMMENTurl = {https://doi.org/10.1007/978-3-642-03034-5_12}, doi = {10.1007/978-3-642-03034-5_12}, timestamp = {Tue, 14 May 2019 10:00:37 +0200}, biburl = {https://dblp.org/rec/conf/dsl/LinckeJZI09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/jfp/MuKJ09, author = {Shin{-}Cheng Mu and Hsiang{-}Shang Ko and Patrik Jansson}, title = {Algebra of programming in {Agda}: Dependent types for relational program derivation}, journal = {J. Funct. Program.}, volume = 19, number = 5, pages = {545--579}, year = 2009, publisher = {Cambridge University Press}, COMMENTurl = {https://doi.org/10.1017/S0956796809007345}, doi = {10.1017/S0956796809007345}, timestamp = {Fri, 27 Mar 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/jfp/MuKJ09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/esop/BernardyJC10, author = {Jean{-}Philippe Bernardy and Patrik Jansson and Koen Claessen}, editor = {Andrew D. Gordon}, title = {Testing Polymorphic Properties}, shortbooktitle={ESOP 2010}, booktitle = {Programming Languages and Systems, 19th European Symposium on Programming, {ESOP} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = 6012, pages = {125--144}, publisher = {Springer}, year = 2010, COMMENTurl = {https://doi.org/10.1007/978-3-642-11957-6_8}, doi = {10.1007/978-3-642-11957-6_8}, timestamp = {Tue, 14 May 2019 10:00:41 +0200}, biburl = {https://dblp.org/rec/conf/esop/BernardyJC10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/jfp/BernardyJZS10, author = {Jean{-}Philippe Bernardy and Patrik Jansson and Marcin Zalewski and Sibylle Schupp}, title = {Generic programming with {C++} concepts and {Haskell} type classes - a comparison}, journal = {J. Funct. Program.}, volume = 20, number = {3-4}, pages = {271--302}, year = 2010, publisher = {Cambridge University Press}, COMMENTurl = {https://doi.org/10.1017/S095679681000016X}, doi = {10.1017/S095679681000016X}, timestamp = {Tue, 06 Jun 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/BernardyJZS10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/icfp/BernardyJP10, author = {Jean{-}Philippe Bernardy and Patrik Jansson and Ross Paterson}, editor = {Paul Hudak and Stephanie Weirich}, title = {Parametricity and dependent types}, booktitle = {Proceeding of the 15th {ACM} {SIGPLAN} international conference on Functional programming, {ICFP} 2010, Baltimore, Maryland, USA, September 27-29, 2010}, pages = {345--356}, publisher = {{ACM}}, year = 2010, COMMENTurl = {https://doi.org/10.1145/1863543.1863592}, doi = {10.1145/1863543.1863592}, timestamp = {Tue, 22 Jun 2021 17:10:56 +0200}, biburl = {https://dblp.org/rec/conf/icfp/BernardyJP10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/haskell/DuregardJ11, author = {Jonas Dureg{\aa}rd and Patrik Jansson}, editor = {Koen Claessen}, title = {Embedded parser generators}, booktitle = {Proceedings of the 4th {ACM} {SIGPLAN} Symposium on {Haskell}, {Haskell} 2011, Tokyo, Japan, 22 September 2011}, pages = {107--117}, publisher = {{ACM}}, year = 2011, COMMENTurl = {https://doi.org/10.1145/2034675.2034689}, doi = {10.1145/2034675.2034689}, timestamp = {Thu, 24 Jun 2021 16:19:30 +0200}, biburl = {https://dblp.org/rec/conf/haskell/DuregardJ11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/erlang/AmaralFJ11, author = {Cl{\'{a}}udio Amaral and M{\'{a}}rio Florido and Patrik Jansson}, editor = {Kenji Rikitake and Erik Stenman}, title = {Interfacing dynamically typed languages and the {Why} tool: reasoning about lists and tuples}, booktitle = {Proceedings of the 10th {ACM} {SIGPLAN} workshop on Erlang, Tokyo, Japan, September 23, 2011}, pages = {92--93}, publisher = {{ACM}}, year = 2011, COMMENTurl = {https://doi.org/10.1145/2034654.2034673}, doi = {10.1145/2034654.2034673}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/erlang/AmaralFJ11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/jfp/BernardyJP12, author = {Jean{-}Philippe Bernardy and Patrik Jansson and Ross Paterson}, title = {Proofs for free - Parametricity for dependent types}, journal = {J. Funct. Program.}, volume = 22, number = 2, pages = {107--152}, year = 2012, publisher = {Cambridge University Press}, COMMENTurl = {https://doi.org/10.1017/S0956796812000056}, doi = {10.1017/S0956796812000056}, timestamp = {Tue, 06 Jun 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/BernardyJP12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/ifl/IonescuJ12, author = {Cezar Ionescu and Patrik Jansson}, editor = {Ralf Hinze}, title = {Dependently-Typed Programming in Scientific Computing - Examples from Economic Modelling}, booktitle = {Implementation and Application of Functional Languages - 24th International Symposium, {IFL} 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = 8241, pages = {140--156}, publisher = {Springer}, year = 2012, COMMENTurl = {https://doi.org/10.1007/978-3-642-41582-1_9}, doi = {10.1007/978-3-642-41582-1_9}, timestamp = {Tue, 14 May 2019 10:00:35 +0200}, biburl = {https://dblp.org/rec/conf/ifl/IonescuJ12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/haskell/JeuringJA12, author = {Johan Jeuring and Patrik Jansson and Cl{\'{a}}udio Amaral}, editor = {Janis Voigtl{\"{a}}nder}, title = {Testing type class laws}, booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Symposium on {Haskell}, {Haskell} 2012, Copenhagen, Denmark, 13 September 2012}, shortbooktitle1 ={Proceedings of the 2012 {Haskell} Symposium}, shortbooktitle2 ={Haskell Symposium}, pages = {49--60}, publisher = {{ACM}}, year = 2012, COMMENTurl = {https://doi.org/10.1145/2364506.2364514}, doi = {10.1145/2364506.2364514}, timestamp = {Thu, 24 Jun 2021 16:19:29 +0200}, biburl = {https://dblp.org/rec/conf/haskell/JeuringJA12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/haskell/DuregardJW12, author = {Jonas Dureg{\aa}rd and Patrik Jansson and Meng Wang}, editor = {Janis Voigtl{\"{a}}nder}, title = {Feat: functional enumeration of algebraic types}, booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Symposium on {Haskell}, {Haskell} 2012, Copenhagen, Denmark, 13 September 2012}, shortbooktitle={Haskell 2012}, pages = {61--72}, publisher = {{ACM}}, year = 2012, COMMENTurl = {https://doi.org/10.1145/2364506.2364515}, doi = {10.1145/2364506.2364515}, timestamp = {Thu, 24 Jun 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/haskell/DuregardJW12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/types/IonescuJ11, author = {Cezar Ionescu and Patrik Jansson}, editor = {Nils Anders Danielsson and Bengt Nordstr{\"{o}}m}, title = {Testing versus proving in climate impact research}, booktitle = {18th International Workshop on Types for Proofs and Programs, {TYPES} 2011, September 8-11, 2011, Bergen, Norway}, series = {LIPIcs}, volume = 19, pages = {41--54}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = 2011, COMMENTurl = {https://doi.org/10.4230/LIPIcs.TYPES.2011.41}, doi = {10.4230/LIPIcs.TYPES.2011.41}, timestamp = {Tue, 11 Feb 2020 15:52:14 +0100}, biburl = {https://dblp.org/rec/conf/types/IonescuJ11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/icfp/ErikssonJ16, author = {Sandberg Eriksson, Adam and Jansson, Patrik}, editor = {James Chapman and Wouter Swierstra}, title = {An {Agda} formalisation of the transitive closure of block matrices (extended abstract)}, booktitle = {Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016}, pages = {60--61}, publisher = {{ACM}}, year = 2016, COMMENTurl = {https://doi.org/10.1145/2976022.2976025}, doi = {10.1145/2976022.2976025}, ISBN = 9781450344357, timestamp = {Mon, 16 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icfp/ErikssonJ16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/corr/BernardyJ16, author = {Jean{-}Philippe Bernardy and Patrik Jansson}, title = {Certified Context-Free Parsing: A formalisation of {Valiant}'s Algorithm in {Agda}}, SHORTjournal = {Log. Methods Comput. Sci.}, journal = {Logical Methods in Computer Science}, volume = 12, number = 2, year = 2016, COMMENTurl = {https://doi.org/10.2168/LMCS-12(2:6)2016}, doi = {10.2168/LMCS-12(2:6)2016}, timestamp = {Thu, 25 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BernardyJ16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, abstract = "Valiant (1975) has developed an algorithm for recognition of context free languages. As of today, it remains the algorithm with the best asymptotic complexity for this purpose. In this paper, we present an algebraic specification, implementation, and proof of correctness of a generalisation of Valiant's algorithm. The generalisation can be used for recognition, parsing or generic calculation of the transitive closure of upper triangular matrices. The proof is certified by the Agda proof assistant. The certification is representative of state-of-the-art methods for specification and proofs in proof assistants based on type-theory. As such, this paper can be read as a tutorial for the Agda system.", note = "arXiv:1601.07724" } @inproceedings{DBLP:journals/corr/IonescuJ16, author = {Cezar Ionescu and Patrik Jansson}, editor = {Johan Jeuring and Jay McCarthy}, title = {Domain-Specific Languages of Mathematics: Presenting Mathematical Analysis Using Functional Programming}, booktitle = {Proceedings of the 4th and 5th International Workshop on Trends in Functional Programming in Education, {TFPIE} 2016, Sophia-Antipolis, France, and University of Maryland, College Park, MD, USA, June 2, 2015, and June 7, 2016}, series = {{EPTCS}}, volume = 230, pages = {1--15}, year = 2016, COMMENTurl = {https://doi.org/10.4204/EPTCS.230.1}, doi = {10.4204/EPTCS.230.1}, timestamp = {Mon, 16 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/IonescuJ16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, archivePrefix ="arXiv", eprint = "1611.09475", primaryClass = "cs.CY", abstract = "We present the approach underlying a course on ``Domain-Specific Languages of Mathematics'', currently being developed at Chalmers in response to difficulties faced by third-year students in learning and applying classical mathematics (mainly real and complex analysis). The main idea is to encourage the students to approach mathematical domains from a functional programming perspective: to identify the main functions and types involved and, when necessary, to introduce new abstractions; to give calculational proofs; to pay attention to the syntax of the mathematical expressions; and, finally, to organise the resulting functions and types in domain-specific languages.", } @article{DBLP:journals/jfp/BottaJI17, author = {Nicola Botta and Patrik Jansson and Cezar Ionescu}, title = {Contributions to a computational theory of policy advice and avoidability}, journal = {J. Funct. Program.}, volume = 27, pages = {e23}, year = 2017, publisher = {Cambridge University Press}, COMMENTurl = {https://doi.org/10.1017/S0956796817000156}, doi = {10.1017/S0956796817000156}, timestamp = {Mon, 16 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/BottaJI17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/corr/BottaJICB16, author = {Nicola Botta and Patrik Jansson and Cezar Ionescu and David R. Christiansen and Edwin C. Brady}, title = {Sequential decision problems, dependent types and generic solutions}, journal = {Log. Methods Comput. Sci.}, volume = 13, number = 1, year = 2017, COMMENTurl = {https://doi.org/10.23638/LMCS-13(1:7)2017}, doi = {10.23638/LMCS-13(1:7)2017}, timestamp = {Thu, 25 Jun 2020 01:00:00 +0200}, abstract = "We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.", publisher = {Episciences. org}, biburl = {https://dblp.org/rec/journals/corr/BottaJICB16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, note = "arXiv:1610.07145" } @inproceedings{DBLP:conf/icfp/AlgehedJ17, author = {Maximilian Algehed and Patrik Jansson}, editor = {Phil Trinder and Cosmin E. Oancea}, title = {VisPar: visualising dataflow graphs from the Par Monad}, booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} International Workshop on Functional High-Performance Computing, FHPC@ICFP 2017, Oxford, UK, September 7, 2017}, pages = {24--29}, publisher = {{ACM}}, year = 2017, COMMENTurl = {https://doi.org/10.1145/3122948.3122953}, doi = {10.1145/3122948.3122953}, timestamp = {Mon, 12 Jul 2021 15:34:15 +0200}, biburl = {https://dblp.org/rec/conf/icfp/AlgehedJ17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{botta2018impact, title = {The impact of uncertainty on optimal emission policies}, author = {Botta, Nicola and Jansson, Patrik and Ionescu, Cezar}, journal = {Earth System Dynamics}, volume = 9, number = 2, pages = {525--542}, year = 2018, publisher = {Copernicus GmbH}, doi = {10.5194/esd-9-525-2018} } @inproceedings{DBLP:conf/sfp/AlgehedJEG18, author = {Maximilian Algehed and Patrik Jansson and S{\'{o}}lr{\'{u}}n Halla Einarsd{\'{o}}ttir and Alex Gerdes}, editor = {Michal H. Palka and Magnus O. Myreen}, title = {Saint: An API-Generic Type-Safe Interpreter}, booktitle = {Trends in Functional Programming - 19th International Symposium, {TFP} 2018, Gothenburg, Sweden, June 11-13, 2018, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = 11457, pages = {94--113}, publisher = {Springer}, year = 2018, COMMENTurl = {https://doi.org/10.1007/978-3-030-18506-0_5}, doi = {10.1007/978-3-030-18506-0_5}, timestamp = {Mon, 03 Jun 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/sfp/AlgehedJEG18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/isola/IonescuJB18, author = {Cezar Ionescu and Patrik Jansson and Nicola Botta}, editor = {Tiziana Margaria and Bernhard Steffen}, title = {Type Theory as a Framework for Modelling and Programming}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = 11244, pages = {119--133}, publisher = {Springer}, year = 2018, COMMENTurl = {https://doi.org/10.1007/978-3-030-03418-4_8}, doi = {10.1007/978-3-030-03418-4_8}, timestamp = {Tue, 14 May 2019 10:00:41 +0200}, biburl = {https://dblp.org/rec/conf/isola/IonescuJB18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{Krook2019aao, author = {Krook, Robert and Jansson, Patrik}, title = {An Algebra of Sequential Decision Problems: Extended Abstract}, booktitle = {Proceedings of ACM SIGPLAN Workshop on Type-Driven Development (TyDe’19)}, year = 2019, publisher = {ACM}, COMMENT = {\cite{krook2019algebra}}, note = {See also the Technical Report available at \url{https://www.cse.chalmers.se/~patrikj/papers/AlgSDP_Krook_Jansson_2019_TechReport.pdf}.} } @inproceedings{DBLP:journals/corr/abs-1908-01572, author = {Patrik Jansson and S{\'{o}}lr{\'{u}}n Halla Einarsd{\'{o}}ttir and Cezar Ionescu}, editor = {Peter Achten and Heather Miller}, title = {Examples and Results from a {BSc-level} Course on Domain Specific Languages of Mathematics}, booktitle = {Proceedings Seventh International Workshop on Trends in Functional Programming in Education, TFPIE@TFP 2018, Chalmers University, Gothenburg, Sweden, 14th June 2018}, shortbooktitle ={Electronic Proceedings in Theoretical Computer Science, EPTCS}, series = {{EPTCS}}, volume = 295, pages = {79--90}, year = 2018, COMMENTurl = {https://doi.org/10.4204/EPTCS.295.6}, doi = {10.4204/EPTCS.295.6}, timestamp = {Tue, 08 Oct 2019 13:24:16 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-01572.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, abstract = "At the workshop on Trends in Functional Programming in Education (TFPIE) in 2015 Ionescu and Jansson presented the approach underlying the ``Domain Specific Languages of Mathematics'' (DSLsofMath) course even before the first course instance. We were then encouraged to come back to present our experience and the student results. Now, three years later, we have seen three groups of learners attend the course, and the first two groups have also continued on to take challenging courses in the subsequent year. In this paper we present three examples from the course material to set the scene, and we present an evaluation of the student results showing improvements in the pass rates and grades in later courses.", archivePrefix ="arXiv", primaryClass = "cs.PL", eprint = "1908.01572" } @article{DBLP:journals/jfp/BottaBJT21, title = "Extensional equality preservation and verified generic programming", author = "Botta, Nicola and Brede, Nuria and Jansson, Patrik and Richter, Tim", abstract = "In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises the question of what useful ADTs for verified functors and monads could look like. The functorial map of many important monads preserves extensional equality. For instance, if $f, g : A \rightarrow B$ are extensionally equal, that is, $\forall x \in A, \ f \ x = g \ x$, then $map \ f : List \ A \rightarrow List \ B$ and $map \ g$ are also extensionally equal. This suggests that preservation of extensional equality could be a useful principle in verified generic programming. We explore this possibility with a minimalist approach: we deal with (the lack of) extensional equality in Martin-{L\"of}'s intensional type theories without extending the theories or using full-fledged setoids. Perhaps surprisingly, this minimal approach turns out to be extremely useful. It allows one to derive simple generic proofs of monadic laws but also verified, generic results in dynamical systems and control theory. In turn, these results avoid tedious code duplication and ad-hoc proofs. Thus, our work is a contribution towards pragmatic, verified generic programming.", journal = {J. Funct. Program.}, publisher = {Cambridge University Press}, doi = {10.1017/S0956796821000204}, COMMENTurl = {https://doi.org/10.1017/S0956796821000204}, volume = 31, year = 2021, note = "arXiv:2008.02123" } @Book{JanssonIonescuBernardyDSLsofMathBook2022, author = {Patrik Jansson and Cezar Ionescu and Jean-Philippe Bernardy}, title = {Domain-Specific Languages of Mathematics}, publisher = {College Publications}, pages = 268, language = {English}, year = 2022, URL = {https://www.collegepublications.co.uk/computing/?00024}, ISBN = {978-1-84890-388-3}, volume = 24, series = {Texts in Computing}, month = JAN, abstract = {The main idea behind this book is to encourage readers to approach mathematical domains from a functional programming perspective: to identify the main functions and types involved and, when necessary, to introduce new abstractions; to give calculational proofs; to pay attention to the syntax of the mathematical expressions; and, finally, to organize the resulting functions and types in domain-specific languages. The book is recommended for developers who are learning mathematics and would like to use Haskell to make sense of definitions and theorems. It is also a book for the mathematically interested who wants to explore functional programming and domain-specific languages. The book helps put into perspective the domains of Mathematics and Functional Programming and shows how Computer Science and Mathematics are usefully taught together.} }