paper.bib

@inproceedings{abott2003categories,
  title = {Categories of {{Containers}}},
  doi = {10.1007/3-540-36576-1},
  booktitle = {Proceedings of {{Foundations}} of {{Software Science}} and {{Computation Structures}}},
  publisher = {{Springer-Verlag}},
  author = {Abott, Michael and Altenkirch, Thorsten and Ghani, Neil},
  year = {2003},
  pages = {23-38}
}

@inproceedings{hughes2000quickcheck,
  title = {{{QuickCheck}}: {{A Lightweight Tool}} for {{Random Testing}} of {{Haskell Programs}}},
  doi = {10.1145/351240.351266},
  booktitle = {Proceedings of the 5th {{ACM SIGPLAN International Conference}} on {{Functional Programming}}},
  publisher = {{ACM}},
  author = {Hughes, John and Claessen, Koen},
  year = {2000},
  pages = {268--279}
}

@inproceedings{kiselyov2015freer,
  title = {Freer {{Monads}}, {{More Extensible Effects}}},
  doi = {10.1145/2804302.2804319},
  booktitle = {Proceedings of the 2015 {{ACM SIGPLAN Symposium}} on {{Haskell}}},
  publisher = {{ACM}},
  author = {Kiselyov, Oleg and Ishii, Hiromi},
  year = {2015},
  keywords = {Kan extension,coroutine,effect handler,effect interaction,free monad,open union,type and effect system},
  pages = {94--105}
}

@inproceedings{uustalu2017container,
  title = {Container {{Combinatorics}}: {{Monads}} and {{Lax Monoidal Functors}}},
  doi = {10.1007/978-3-319-68953-1},
  booktitle = {Topics in {{Theoretical Computer Science}}},
  publisher = {{Springer International Publishing}},
  author = {Uustalu, Tarmo},
  year = {2017},
  pages = {91-105}
}

@book{chlipala2011certified,
  title = {Certified {{Programming}} with {{Dependent Types}}},
  publisher = {{MIT Press New York}},
  author = {Chlipala, Adam},
  year = {2011}
}

@misc{coquand2013positive,
  title = {Agda Mailing List},
  howpublished = {https://lists.chalmers.se/pipermail/agda/2013/006189.html},
  author = {Coquand, Thierry and Stump, Aaron and Jedynak, Wojciech},
  month = dec,
  year = {2013}
}

@incollection{altenkirch2007generic,
  series = {LNCS},
  title = {Generic {{Programming}} with {{Dependent Types}}},
  booktitle = {International {{Spring School}}},
  publisher = {{Springer-Verlag}},
  author = {Altenkirch, Thorsten and McBride, Conor and Morris, Peter},
  year = {2006},
  pages = {209--257},
  doi = {10.1007/978-3-540-76786-2}
}

@inproceedings{christiansen2010free,
  title = {Free {{Theorems For Functional Logic Programs}}},
  doi = {10.1145/1707790.1707797},
  booktitle = {Proceedings of the 4th {{ACM SIGPLAN Workshop}} on {{Programming Languages Meets Program Verification}}},
  publisher = {{ACM}},
  author = {Christiansen, Jan and Seidel, Daniel and Voigtl\"ander, Janis},
  year = {2010},
  pages = {39-48},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QJy4uLy4uL1BhcGVycy9DdXJyeS9wMzktY2hyaXN0aWFuc2VuLnBkZtIXCxgZV05TLmRhdGFPEQGyAAAAAAGyAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADSvOLdSCsAAAAWx3oUcDM5LWNocmlzdGlhbnNlbi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAGpsUNNr0sYAAAAAAAAAAAACAAMAAAkgAAAAAAAAAAAAAAAAAAAABUN1cnJ5AAAQAAgAANK81M0AAAARAAgAANNrtqYAAAABABQAFsd6ABbHdgAJXXYACV11AAYsowACAEdNYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AEN1cnJ5OgBwMzktY2hyaXN0aWFuc2VuLnBkZgAADgAqABQAcAAzADkALQBjAGgAcgBpAHMAdABpAGEAbgBzAGUAbgAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIANVVzZXJzL2phYy9Eb2N1bWVudHMvUGFwZXJzL0N1cnJ5L3AzOS1jaHJpc3RpYW5zZW4ucGRmAAATAAEvAAAVAAIACv//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOALgAvQDFAnsCfQKCAo0ClgKkAqgCrwK4Ar0CygLNAt8C4gLnAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAuk=}
}

@inproceedings{mehner2014parametricity,
  title = {Parametricity and {{Proving Free Theorems}} for {{Functional}}-{{Logic Languages}}},
  doi = {10.1145/2643135.2643147},
  booktitle = {Proceedings of the 16th {{International Symposium}} on {{Principles}} and {{Practice}} of {{Declarative Programming}}},
  publisher = {{ACM}},
  author = {Mehner, Stefan and Seidel, Daniel and Stra\ss{}burger, Lutz and Voigtl\"ander, Janis},
  year = {2014},
  keywords = {free theorems,Curry,functional logic programming},
  pages = {19-30},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QZS4uLy4uL1BhcGVycy9GcmVlIFRoZW9yZW1zL1BhcmFtZXRyaWNpdHkgYW5kIFByb3ZpbmcgRnJlZSBUaGVvcmVtcyBmb3IgRnVuY3Rpb25hbC1Mb2dpYyBMYW5ndWFnZXMucGRm0hcLGBlXTlMuZGF0YU8RAnYAAAAAAnYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAANK84t1IKwAAAG4hpB9QYXJhbWV0cmljaXR5IGFuZCBQIzExMjBBQjcucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABEgq31MMfBVBERiAAAAAAAAIAAwAACSAAAAAAAAAAAAAAAAAAAAANRnJlZSBUaGVvcmVtcwAAEAAIAADSvNTNAAAAEQAIAADUwxD1AAAAAQAUAG4hpAAWx3YACV12AAlddQAGLKMAAgBaTWFjaW50b3NoIEhEOlVzZXJzOgBqYWM6AERvY3VtZW50czoAUGFwZXJzOgBGcmVlIFRoZW9yZW1zOgBQYXJhbWV0cmljaXR5IGFuZCBQIzExMjBBQjcucGRmAA4AlgBKAFAAYQByAGEAbQBlAHQAcgBpAGMAaQB0AHkAIABhAG4AZAAgAFAAcgBvAHYAaQBuAGcAIABGAHIAZQBlACAAVABoAGUAbwByAGUAbQBzACAAZgBvAHIAIABGAHUAbgBjAHQAaQBvAG4AYQBsAC0ATABvAGcAaQBjACAATABhAG4AZwB1AGEAZwBlAHMALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAHNVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9GcmVlIFRoZW9yZW1zL1BhcmFtZXRyaWNpdHkgYW5kIFByb3ZpbmcgRnJlZSBUaGVvcmVtcyBmb3IgRnVuY3Rpb25hbC1Mb2dpYyBMYW5ndWFnZXMucGRmAAATAAEvAAAVAAIACv//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAPYA+wEDA30DfwOEA48DmAOmA6oDsQO6A78DzAPPA+ED5APpAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAA+s=}
}

@inproceedings{verbruggen2008polytypic,
  title = {Polytypic {{Programming}} in {{Coq}}},
  doi = {10.1145/1411318.1411326},
  booktitle = {Proceedings of the {{ACM SIGPLAN Workshop}} on {{Generic Programming}}},
  publisher = {{ACM}},
  author = {Verbruggen, Wendy and {de Vries}, Edsko and Hughes, Arthur},
  year = {2008},
  pages = {49-60}
}

@inproceedings{coquand1990inductively,
  title = {Inductively {{Defined Types}}},
  doi = {10.1007/3-540-52335-9_47},
  booktitle = {Proceedings of the {{International Conference}} on {{Computer Logic}}},
  publisher = {{Springer-Verlag}},
  author = {Coquand, Thierry and Paulin, Christine},
  year = {1988},
  pages = {50-66}
}

@inproceedings{danielsson2006fast,
  title = {Fast and {{Loose Reasoning}} Is {{Morally Correct}}},
  doi = {10.1145/1111320.1111056},
  booktitle = {Conference {{Record}} of the 33rd {{ACM SIGPLAN}}-{{SIGACT Symposium}} on {{Principles}} of {{Programming Languages}}},
  publisher = {{ACM}},
  author = {Danielsson, Nils Anders and Hughes, John and Jansson, Patrik and Gibbons, Jeremy},
  year = {2006},
  pages = {206-217},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QRi4uLy4uL1BhcGVycy9SZWFzb25pbmcvRmFzdCBhbmQgTG9vc2UgUmVhc29uaW5nIGlzIE1vcmFsbHkgQ29ycmVjdC5wZGbSFwsYGVdOUy5kYXRhTxECGAAAAAACGAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAA0rzi3UgrAAACNWYvH0Zhc3QgYW5kIExvb3NlIFJlYXMjMjM1NjYwRS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAI1Zg7WxViqUERGIAAAAAAAAgADAAAJIAAAAAAAAAAAAAAAAAAAAAlSZWFzb25pbmcAABAACAAA0rzUzQAAABEACAAA1sVKmgAAAAEAFAI1Zi8AFsd2AAlddgAJXXUABiyjAAIAVk1hY2ludG9zaCBIRDpVc2VyczoAamFjOgBEb2N1bWVudHM6AFBhcGVyczoAUmVhc29uaW5nOgBGYXN0IGFuZCBMb29zZSBSZWFzIzIzNTY2MEUucGRmAA4AYAAvAEYAYQBzAHQAIABhAG4AZAAgAEwAbwBvAHMAZQAgAFIAZQBhAHMAbwBuAGkAbgBnACAAaQBzACAATQBvAHIAYQBsAGwAeQAgAEMAbwByAHIAZQBjAHQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAFRVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9SZWFzb25pbmcvRmFzdCBhbmQgTG9vc2UgUmVhc29uaW5nIGlzIE1vcmFsbHkgQ29ycmVjdC5wZGYAEwABLwAAFQACAAr//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgDXANwA5AMAAwIDBwMSAxsDKQMtAzQDPQNCA08DUgNkA2cDbAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAANu}
}

@inproceedings{abel2005verifying,
  title = {Verifying {{Haskell Programs Using Constructive Type Theory}}},
  doi = {10.1145/1088348.1088355},
  booktitle = {Proceedings of the 2005 {{ACM SIGPLAN Workshop}} on {{Haskell}}},
  publisher = {{ACM}},
  author = {Abel, Andreas and Benke, Marcin and Bove, Ana and Hughes, John and Norell, Ulf},
  year = {2005},
  pages = {62-73},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QWy4uLy4uL1BhcGVycy9UaGVvcmVtIFByb3ZpbmcvVmVyaWZ5aW5nIEhhc2tlbGwgcHJvZ3JhbXMgdXNpbmcgY29uc3RydWN0aXZlIHR5cGUgdGhlb3J5IC5wZGbSFwsYGVdOUy5kYXRhTxECWAAAAAACWAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAA0rzi3UgrAAAAxsF3H1ZlcmlmeWluZyBIYXNrZWxsIHByIzE2Qzc5RS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAWx57SOaQOAAAAAAAAAAAAAgADAAAJIAAAAAAAAAAAAAAAAAAAAA9UaGVvcmVtIFByb3ZpbmcAABAACAAA0rzUzQAAABEACAAA0jmH7gAAAAEAFADGwXcAFsd2AAlddgAJXXUABiyjAAIAXE1hY2ludG9zaCBIRDpVc2VyczoAamFjOgBEb2N1bWVudHM6AFBhcGVyczoAVGhlb3JlbSBQcm92aW5nOgBWZXJpZnlpbmcgSGFza2VsbCBwciMxNkM3OUUucGRmAA4AfgA+AFYAZQByAGkAZgB5AGkAbgBnACAASABhAHMAawBlAGwAbAAgAHAAcgBvAGcAcgBhAG0AcwAgAHUAcwBpAG4AZwAgAGMAbwBuAHMAdAByAHUAYwB0AGkAdgBlACAAdAB5AHAAZQAgAHQAaABlAG8AcgB5ACAALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAGlVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9UaGVvcmVtIFByb3ZpbmcvVmVyaWZ5aW5nIEhhc2tlbGwgcHJvZ3JhbXMgdXNpbmcgY29uc3RydWN0aXZlIHR5cGUgdGhlb3J5IC5wZGYAABMAAS8AABUAAgAK//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4A7ADxAPkDVQNXA1wDZwNwA34DggOJA5IDlwOkA6cDuQO8A8EAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAADww==}
}

@techreport{mcadam1997wraps,
  title = {That {{About Wraps It Up}}},
  number = {ECS--LFCS--97--375},
  institution = {{Department of Computer Science, University of Edinburgh}},
  author = {McAdam, Bruce J.},
  month = nov,
  year = {1997},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QLS4uLy4uL1BhcGVycy9UeXBlcy9UaGF0IGFib3V0IHdyYXBzIGl0IHVwLnBkZtIXCxgZV05TLmRhdGFPEQHKAAAAAAHKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADSvOLdSCsAAACo1N4aVGhhdCBhYm91dCB3cmFwcyBpdCB1cC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAARP6k9THO35QREYgAAAAAAACAAMAAAkgAAAAAAAAAAAAAAAAAAAABVR5cGVzAAAQAAgAANK81M0AAAARAAgAANTHLW4AAAABABQAqNTeABbHdgAJXXYACV11AAYsowACAE1NYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AFR5cGVzOgBUaGF0IGFib3V0IHdyYXBzIGl0IHVwLnBkZgAADgA2ABoAVABoAGEAdAAgAGEAYgBvAHUAdAAgAHcAcgBhAHAAcwAgAGkAdAAgAHUAcAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAO1VzZXJzL2phYy9Eb2N1bWVudHMvUGFwZXJzL1R5cGVzL1RoYXQgYWJvdXQgd3JhcHMgaXQgdXAucGRmAAATAAEvAAAVAAIACv//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAL4AwwDLApkCmwKgAqsCtALCAsYCzQLWAtsC6ALrAv0DAAMFAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAwc=}
}

@inproceedings{fischer2009purely,
  title = {Purely {{Functional Lazy Non}}-Deterministic {{Programming}}},
  doi = {10.1145/1596550.1596556},
  booktitle = {Proceedings of the 14th {{ACM SIGPLAN International Conference}} on {{Functional Programming}}},
  publisher = {{ACM}},
  author = {Fischer, Sebastian and Kiselyov, Oleg and Shan, Chung-chieh},
  year = {2009},
  pages = {11-22},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QSy4uLy4uL1BhcGVycy9DdXJyeS9QdXJlbHkgRnVuY3Rpb25hbCBMYXp5IE5vbi1kZXRlcm1pbmlzdGljIFByb2dyYW1taW5nLnBkZtIXCxgZV05TLmRhdGFPEQIoAAAAAAIoAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADSvOLdSCsAAAAWx3ofUHVyZWx5IEZ1bmN0aW9uYWwgTCMxMUQ1RTBCLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAR1eC9TTajVQREYgAAAAAAACAAMAAAkgAAAAAAAAAAAAAAAAAAAABUN1cnJ5AAAQAAgAANK81M0AAAARAAgAANTTXCUAAAABABQAFsd6ABbHdgAJXXYACV11AAYsowACAFJNYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AEN1cnJ5OgBQdXJlbHkgRnVuY3Rpb25hbCBMIzExRDVFMEIucGRmAA4AcgA4AFAAdQByAGUAbAB5ACAARgB1AG4AYwB0AGkAbwBuAGEAbAAgAEwAYQB6AHkAIABOAG8AbgAtAGQAZQB0AGUAcgBtAGkAbgBpAHMAdABpAGMAIABQAHIAbwBnAHIAYQBtAG0AaQBuAGcALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAFlVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9DdXJyeS9QdXJlbHkgRnVuY3Rpb25hbCBMYXp5IE5vbi1kZXRlcm1pbmlzdGljIFByb2dyYW1taW5nLnBkZgAAEwABLwAAFQACAAr//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgDcAOEA6QMVAxcDHAMnAzADPgNCA0kDUgNXA2QDZwN5A3wDgQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAOD}
}

@inproceedings{keuchel2013generic,
  title = {Generic {{Datatypes}} \`a La {{Carte}}},
  doi = {10.1145/2502488.2502491},
  booktitle = {Proceedings of the 9th {{ACM SIGPLAN Workshop}} on {{Generic Programming}}},
  publisher = {{ACM}},
  author = {Keuchel, Steven and Schrijvers, Tom},
  year = {2013},
  keywords = {datatype-generic programming,fixed points,mechanized meta-theory,modularity},
  pages = {13-24},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QNy4uLy4uL1BhcGVycy9HZW5lcmljcy9HZW5lcmljIERhdGF0eXBlcyBhYCBsYSBDYXJ0ZS5wZGbSFwsYGVdOUy5kYXRhTxEB7AAAAAAB7AACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAA0rzi3UgrAAACGfwDH0dlbmVyaWMgRGF0YXR5cGVzIGEjMjE5QUZFNi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAIZr+bWjRJfUERGIAAAAAAAAgADAAAJIAAAAAAAAAAAAAAAAAAAAAhHZW5lcmljcwAQAAgAANK81M0AAAARAAgAANaNBE8AAAABABQCGfwDABbHdgAJXXYACV11AAYsowACAFVNYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AEdlbmVyaWNzOgBHZW5lcmljIERhdGF0eXBlcyBhIzIxOUFGRTYucGRmAAAOAEQAIQBHAGUAbgBlAHIAaQBjACAARABhAHQAYQB0AHkAcABlAHMAIABhAGAAIABsAGEAIABDAGEAcgB0AGUALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEVVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9HZW5lcmljcy9HZW5lcmljIERhdGF0eXBlcyBhYCBsYSBDYXJ0ZS5wZGYAABMAAS8AABUAAgAK//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AyADNANUCxQLHAswC1wLgAu4C8gL5AwIDBwMUAxcDKQMsAzEAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAADMw==}
}

@inproceedings{johann2004free,
  title = {Free {{Theorems}} in the {{Presence}} of Seq},
  doi = {10.1145/982962.964010},
  booktitle = {Proceedings of the 31st {{ACM SIGPLAN}}-{{SIGACT Symposium}} on {{Principles}} of {{Programming Languages}}},
  publisher = {{ACM}},
  author = {Johann, Patricia and Voigtl\"ander, Janis},
  year = {2004},
  pages = {99-110},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QQy4uLy4uL1BhcGVycy9GcmVlIFRoZW9yZW1zL0ZyZWUgVGhlb3JlbXMgaW4gdGhlIFByZXNlbmNlIG9mIHNlcS5wZGbSFwsYGVdOUy5kYXRhTxECEAAAAAACEAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAA0rzi3UgrAAAAbiGkH0ZyZWUgVGhlb3JlbXMgaW4gdGgjMUVEQzFENS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAHtwdXWIl3uAAAAAAAAAAAAAgADAAAJIAAAAAAAAAAAAAAAAAAAAA1GcmVlIFRoZW9yZW1zAAAQAAgAANK81M0AAAARAAgAANYiT94AAAABABQAbiGkABbHdgAJXXYACV11AAYsowACAFpNYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AEZyZWUgVGhlb3JlbXM6AEZyZWUgVGhlb3JlbXMgaW4gdGgjMUVEQzFENS5wZGYADgBSACgARgByAGUAZQAgAFQAaABlAG8AcgBlAG0AcwAgAGkAbgAgAHQAaABlACAAUAByAGUAcwBlAG4AYwBlACAAbwBmACAAcwBlAHEALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAFFVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9GcmVlIFRoZW9yZW1zL0ZyZWUgVGhlb3JlbXMgaW4gdGhlIFByZXNlbmNlIG9mIHNlcS5wZGYAABMAAS8AABUAAgAK//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4A1ADZAOEC9QL3AvwDBwMQAx4DIgMpAzIDNwNEA0cDWQNcA2EAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAADYw==}
}

@article{swierstra2008data,
  title = {Data {{Types}} \`a La {{Carte}}},
  volume = {18},
  doi = {10.1017/S0956796808006758},
  number = {4},
  journal = {Journal of Functional Programming},
  author = {Swierstra, Wouter},
  year = {2008},
  pages = {423-436},
  publisher = {{Cambridge University Press}},
  location = {New York, NY, USA},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QMi4uLy4uL1BhcGVycy9EYXRhIFN0cnVjdHVyZXMvRGF0YVR5cGVzQUxhQ2FydGUucGRm0hcLGBlXTlMuZGF0YU8RAdIAAAAAAdIAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAANK84t1IKwAAAKjdYhVEYXRhVHlwZXNBTGFDYXJ0ZS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAqYCM1A/uGgAAAAAAAAAAAAIAAwAACSAAAAAAAAAAAAAAAAAAAAAPRGF0YSBTdHJ1Y3R1cmVzAAAQAAgAANK81M0AAAARAAgAANQP0foAAAABABQAqN1iABbHdgAJXXYACV11AAYsowACAFJNYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AERhdGEgU3RydWN0dXJlczoARGF0YVR5cGVzQUxhQ2FydGUucGRmAA4ALAAVAEQAYQB0AGEAVAB5AHAAZQBzAEEATABhAEMAYQByAHQAZQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAQFVzZXJzL2phYy9Eb2N1bWVudHMvUGFwZXJzL0RhdGEgU3RydWN0dXJlcy9EYXRhVHlwZXNBTGFDYXJ0ZS5wZGYAEwABLwAAFQACAAr//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgDDAMgA0AKmAqgCrQK4AsECzwLTAtoC4wLoAvUC+AMKAw0DEgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAMU}
}

@inproceedings{dylus2018probabilistic,
  title = {Probabilistic {{Functional Logic Programming}}},
  doi = {10.1007/978-3-319-73305-0},
  booktitle = {Practical {{Aspects}} of {{Declarative Languages}}},
  publisher = {{Springer International Publishing}},
  author = {Dylus, Sandra and Christiansen, Jan and Teegen, Finn},
  year = {2018},
  pages = {3-19},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QWC4uLy4uL1BhcGVycy9GdW5jdGlvbmFsIExvZ2ljIFByb2dyYW1taW5nL1Byb2JhYmlsaXN0aWMgRnVuY3Rpb25hbCBMb2dpYyBQcm9ncmFtbWluZy5wZGbSFwsYGVdOUy5kYXRhTxECTgAAAAACTgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAA0rzi3UgrAAACJsASH1Byb2JhYmlsaXN0aWMgRnVuY3QjMjI2QkZGNy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAImv/fWm3heUERGIAAAAAAAAgADAAAJIAAAAAAAAAAAAAAAAAAAABxGdW5jdGlvbmFsIExvZ2ljIFByb2dyYW1taW5nABAACAAA0rzUzQAAABEACAAA1ptqTgAAAAEAFAImwBIAFsd2AAlddgAJXXUABiyjAAIAaU1hY2ludG9zaCBIRDpVc2VyczoAamFjOgBEb2N1bWVudHM6AFBhcGVyczoARnVuY3Rpb25hbCBMb2dpYyBQcm9ncmFtbWluZzoAUHJvYmFiaWxpc3RpYyBGdW5jdCMyMjZCRkY3LnBkZgAADgBeAC4AUAByAG8AYgBhAGIAaQBsAGkAcwB0AGkAYwAgAEYAdQBuAGMAdABpAG8AbgBhAGwAIABMAG8AZwBpAGMAIABQAHIAbwBnAHIAYQBtAG0AaQBuAGcALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAGZVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9GdW5jdGlvbmFsIExvZ2ljIFByb2dyYW1taW5nL1Byb2JhYmlsaXN0aWMgRnVuY3Rpb25hbCBMb2dpYyBQcm9ncmFtbWluZy5wZGYAEwABLwAAFQACAAr//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgDpAO4A9gNIA0oDTwNaA2MDcQN1A3wDhQOKA5cDmgOsA68DtAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAO2}
}

@inproceedings{svenningsson2002shortcut,
  title = {Shortcut {{Fusion}} for {{Accumulating Parameters}} \& {{Zip}}-like {{Functions}}},
  doi = {10.1145/581478.581491},
  booktitle = {Proceedings of the 7th {{ACM SIGPLAN International Conference}} on {{Functional Programming}}},
  publisher = {{ACM}},
  author = {Svenningsson, Josef},
  year = {2002},
  pages = {124-132},
  bdsk-file-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QaS4uLy4uL1BhcGVycy9Qcm9ncmFtIFRyYW5zZm9ybWF0aW9ucy9TaG9ydGN1dCBGdXNpb24gZm9yIEFjY3VtdWxhdGluZyBQYXJhbWV0ZXJzICYgWmlwLWxpa2UgRnVuY3Rpb25zLnBkZtIXCxgZV05TLmRhdGFPEQKCAAAAAAKCAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADSvOLdSCsAAAIYqFsfU2hvcnRjdXQgRnVzaW9uIGZvciMyMThBODQzLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAhioQ9aLlfNQREYgAAAAAAACAAMAAAkgAAAAAAAAAAAAAAAAAAAAF1Byb2dyYW0gVHJhbnNmb3JtYXRpb25zAAAQAAgAANK81M0AAAARAAgAANaLh+MAAAABABQCGKhbABbHdgAJXXYACV11AAYsowACAGRNYWNpbnRvc2ggSEQ6VXNlcnM6AGphYzoARG9jdW1lbnRzOgBQYXBlcnM6AFByb2dyYW0gVHJhbnNmb3JtYXRpb25zOgBTaG9ydGN1dCBGdXNpb24gZm9yIzIxOEE4NDMucGRmAA4AigBEAFMAaABvAHIAdABjAHUAdAAgAEYAdQBzAGkAbwBuACAAZgBvAHIAIABBAGMAYwB1AG0AdQBsAGEAdABpAG4AZwAgAFAAYQByAGEAbQBlAHQAZQByAHMAIAAmACAAWgBpAHAALQBsAGkAawBlACAARgB1AG4AYwB0AGkAbwBuAHMALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAHdVc2Vycy9qYWMvRG9jdW1lbnRzL1BhcGVycy9Qcm9ncmFtIFRyYW5zZm9ybWF0aW9ucy9TaG9ydGN1dCBGdXNpb24gZm9yIEFjY3VtdWxhdGluZyBQYXJhbWV0ZXJzICYgWmlwLWxpa2UgRnVuY3Rpb25zLnBkZgAAEwABLwAAFQACAAr//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgD6AP8BBwONA48DlAOfA6gDtgO6A8EDygPPA9wD3wPxA/QD+QAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAP7}
}

@article{breitner2018ready,
  title = {Ready, {{Set}}, {{Verify}}! {{Applying Hs}}-to-Coq to {{Real}}-World {{Haskell Code}} ({{Experience Report}})},
  doi = {10.1145/3236784},
  number = {ICFP},
  journal = {Proceedings of the ACM on Programming Languages},
  author = {Breitner, Joachim and {Spector-Zabusky}, Antal and Li, Yao and Rizkallah, Christine and Wiegley, John and Weirich, Stephanie},
  year = {2018},
  keywords = {Haskell,Coq,verification},
  pages = {89:1-89:16}
}

@inproceedings{mcbride2015turingcompleteness,
  title = {Turing-{{Completeness Totally Free}}},
  doi = {10.1007/978-3-319-19797-5_13},
  abstract = {In this paper, I show that general recursive definitions can be represented in the free monad which supports the ‘effect' of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable.},
  booktitle = {Mathematics of {{Program Construction}}},
  publisher = {{Springer International Publishing}},
  author = {McBride, Conor},
  year = {2015},
  pages = {257-275}
}

@inproceedings{letan2018modular,
  title = {Modular {{Verification}} of {{Programs}} with {{Effects}} and {{Effect Handlers}} in {{Coq}}},
  doi = {10.1007/978-3-319-95582-7_20},
  abstract = {Modern computing systems have grown in complexity, and the attack surface has increased accordingly. Even though system components are generally carefully designed and even verified by different groups of people, the composition of these components is often regarded with less attention. This paves the way for ``architectural attacks'', a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its components continues to act as expected. In this article, we introduce FreeSpec, a formalism built upon the key idea that components can be modelled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modelling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.},
  booktitle = {Formal {{Methods}}},
  publisher = {{Springer International Publishing}},
  author = {Letan, Thomas and {R\'egis-Gianas}, Yann and Chifflier, Pierre and Hiet, Guillaume},
  year = {2018},
  pages = {338-354}
}

@article{koh2018interaction,
  archivePrefix = {arXiv},
  eprinttype = {arxiv},
  eprint = {1811.11911},
  primaryClass = {cs.PL},
  title = {From {{C}} to {{Interaction Trees}}:  {{Specifying}}, {{Verifying}}, and {{Testing}} a {{Networked Server}}},
  doi = {10.1145/3293880.3294106},
  journal = {arXiv:1811.11911 [cs.PL]},
  author = {Koh, Niclas and Li, Yao and Li, Yishuai and Xia, Li-yao and Beringer, Lennart and Honor\'e, Wolf and Mansky, William and Pierce, Benjamin C. and Zdancewic, Steve},
  month = nov,
  year = {2018}
}

@article{atkey2015interleaving,
  title = {Interleaving Data and Effects},
  volume = {25},
  doi = {10.1017/S0956796815000209},
  journal = {Journal of Functional Programming},
  author = {Atkey, Robert and Johann, Patricia},
  year = {2015}
}