LIPIcs, Volume 19
TYPES 2011, September 8-11, 2011, Bergen, Norway
Editors: Nils Anders Danielsson and Bengt Nordström
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{danielsson:LIPIcs.TYPES.2019.10, author = {Danielsson, Nils Anders}, title = {{Higher Inductive Type Eliminators Without Paths}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {10:1--10:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-158-0}, ISSN = {1868-8969}, year = {2020}, volume = {175}, editor = {Bezem, Marc and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.10}, URN = {urn:nbn:de:0030-drops-130749}, doi = {10.4230/LIPIcs.TYPES.2019.10}, annote = {Keywords: Cubical Agda, higher inductive types} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
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-dev.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} }
Feedback for Dagstuhl Publishing