Volume

LIPIcs, Volume 19

18th International Workshop on Types for Proofs and Programs (TYPES 2011)



Thumbnail PDF

Event

TYPES 2011, September 8-11, 2011, Bergen, Norway

Editors

Nils Anders Danielsson
Bengt Nordström

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

Documents

No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 19, TYPES'11, Complete Volume

Authors: Nils Anders Danielsson and Bengt Nordström


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-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}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Nils Anders Danielsson and Bengt Nordström


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-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}
}
Document
Non-constructive complex analysis in Coq

Authors: Aloïs Brunel


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-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}
}
Document
Infinitary Rewriting Coinductively

Authors: Jörg Endrullis and Andrew Polonsky


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-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}
}
Document
A new approach to the semantics of model diagrams

Authors: Johan G. Granström


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-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}
}
Document
Testing versus proving in climate impact research

Authors: Cezar Ionescu and Patrik Jansson


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-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}
}
Document
Verification of redecoration for infinite triangular matrices using coinduction

Authors: Ralph Matthes and Celia Picard


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-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}
}

Filters


Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail