Volume
LIPIcs, Volume 19
18th International Workshop on Types for Proofs and Programs (TYPES 2011)
Event
TYPES 2011, September 8-11, 2011, Bergen, NorwayEditors
Publication Details
- published at: 2013-01-21
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-49-1
- DBLP: db/conf/types/types2011
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 19, TYPES'11, Complete Volume
Abstract
LIPIcs, Volume 19, TYPES'11, Complete Volume
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Workshop Organization
Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Non-constructive complex analysis in Coq
Abstract
Winding numbers are fundamental objects arising in algebraic topology, with many applications in non-constructive complex analysis. We present a formalization in Coq of the wind- ing numbers and their main properties. As an application of this development, we also give non-constructive proofs of the following theorems: the Fundamental Theorem of Algebra, the 2-dimensional Brouwer Fixed-Point theorem and the 2-dimensional Borsuk-Ulam theorem.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Infinitary Rewriting Coinductively
Abstract
We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types. The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
A new approach to the semantics of model diagrams
Abstract
Sometimes, a diagram can say more than a thousand lines of code. But, sadly, most of the time, software engineers give up on diagrams after the design phase, and all real work is done in code. The supremacy of code over diagrams would be leveled if diagrams were code. This paper suggests that model and instance diagrams, or, which amounts to the same, class and object diagrams, become first level entities in a suitably expressive programming language, viz., type theory.
The proposed semantics of diagrams is compositional and self-describing, i.e., reflexive, or metacircular. Moreover, it is
well suited for metamodelling and model driven engineering, as it is
possible to prove model transformations correct in type theory. The
encoding into type theory has the additional benefit of making
diagrams immediately useful, given an implementation of type theory.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Testing versus proving in climate impact research
Abstract
Higher-order properties arise naturally in some areas of climate impact research. For example, "vulnerability measures", crucial in assessing the vulnerability to climate change of various regions and entities, must fulfill certain conditions which are best expressed by quantification over all increasing functions of an appropriate type. This kind of property is notoriously difficult to test. However, for the measures used in practice, it is quite easy to encode the property as a dependent type and prove it correct. Moreover, in scientific programming, one is often interested in correctness "up to implication": the program would work as expected, say, if one would use real numbers instead of floating-point values. Such counterfactuals are impossible to test, but again, they can be easily encoded as types and proven. We show examples of such situations (encoded in Agda), encountered in actual vulnerability assessments.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Verification of redecoration for infinite triangular matrices using coinduction
Abstract
Finite triangular matrices with a dedicated type for the diagonal
elements can be profitably represented by a nested data type, i. e., a
heterogeneous family of inductive data types, while infinite
triangular matrices form an example of a nested coinductive type,
which is a heterogeneous family of coinductive data types.
Redecoration for infinite triangular matrices is taken up from
previous work involving the first author, and it is shown that
redecoration forms a comonad with respect to bisimilarity.
The main result, however, is a validation of the original algorithm
against a model based on infinite streams of infinite streams. The
two formulations are even provably equivalent, and the second is
identified as a special instance of the generic cobind operation
resulting from the well-known comultiplication operation on streams
that creates the stream of successive tails of a given stream. Thus,
perhaps surprisingly, the verification of redecoration is easier for
infinite triangular matrices than for their finite counterpart.
All the results have been obtained and are fully formalized in the
current version of the Coq theorem proving environment where these
coinductive datatypes are fully supported since the version 8.1,
released in 2007. Nonetheless, instead of displaying the Coq
development, we have chosen to write the paper in standard
mathematical and type-theoretic language. Thus, it should be
accessible without any specific knowledge about Coq.
Cite as
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)
Copy BibTex To Clipboard
@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}
}