@Proceedings{danielsson_et_al:LIPIcs.TYPES.2011, title = {{LIPIcs, Volume 19, TYPES'11, Complete Volume}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011}, URN = {urn:nbn:de:0030-drops-41132}, doi = {10.4230/LIPIcs.TYPES.2011}, annote = {Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic} } @InProceedings{danielsson_et_al:LIPIcs.TYPES.2011.i, author = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, title = {{Frontmatter, Table of Contents, Preface, Workshop Organization}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {i--vii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.i}, URN = {urn:nbn:de:0030-drops-38957}, doi = {10.4230/LIPIcs.TYPES.2011.i}, annote = {Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization} } @InProceedings{brunel:LIPIcs.TYPES.2011.1, author = {Brunel, Alo\"{i}s}, title = {{Non-constructive complex analysis in Coq}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {1--15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.1}, URN = {urn:nbn:de:0030-drops-38968}, doi = {10.4230/LIPIcs.TYPES.2011.1}, annote = {Keywords: Coq, winding number, complex analysis} } @InProceedings{endrullis_et_al:LIPIcs.TYPES.2011.16, author = {Endrullis, J\"{o}rg and Polonsky, Andrew}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {16--27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.16}, URN = {urn:nbn:de:0030-drops-38971}, doi = {10.4230/LIPIcs.TYPES.2011.16}, annote = {Keywords: infinitary rewriting, coinduction, lambda calculus, standardization} } @InProceedings{granstrom:LIPIcs.TYPES.2011.28, author = {Granstr\"{o}m, Johan G.}, title = {{A new approach to the semantics of model diagrams}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {28--40}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.28}, URN = {urn:nbn:de:0030-drops-38980}, doi = {10.4230/LIPIcs.TYPES.2011.28}, annote = {Keywords: model diagram, modelling, metamodelling, semantics, compositionality, self-description, metacircularity, reflexivity, universal model, MOF, UML} } @InProceedings{ionescu_et_al:LIPIcs.TYPES.2011.41, author = {Ionescu, Cezar and Jansson, Patrik}, title = {{Testing versus proving in climate impact research}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {41--54}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.41}, URN = {urn:nbn:de:0030-drops-38991}, doi = {10.4230/LIPIcs.TYPES.2011.41}, annote = {Keywords: dependently-typed programming, domain-specific languages, climate impact research, formalization} } @InProceedings{matthes_et_al:LIPIcs.TYPES.2011.55, author = {Matthes, Ralph and Picard, Celia}, title = {{Verification of redecoration for infinite triangular matrices using coinduction}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {55--69}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.55}, URN = {urn:nbn:de:0030-drops-39001}, doi = {10.4230/LIPIcs.TYPES.2011.55}, annote = {Keywords: nested datatype, coinduction, theorem proving, Coq} }