18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. i-vii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Aloïs Brunel. Non-constructive complex analysis in Coq. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Jörg Endrullis and Andrew Polonsky. Infinitary Rewriting Coinductively. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 16-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Johan G. Granström. A new approach to the semantics of model diagrams. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 28-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Cezar Ionescu and Patrik Jansson. Testing versus proving in climate impact research. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 41-54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }
Ralph Matthes and Celia Picard. Verification of redecoration for infinite triangular matrices using coinduction. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 55-69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@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} }