eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
0
0
10.4230/LIPIcs.TYPES.2011
article
LIPIcs, Volume 19, TYPES'11, Complete Volume
Danielsson, Nils Anders
Nordström, Bengt
LIPIcs, Volume 19, TYPES'11, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011/LIPIcs.TYPES.2011.pdf
Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
i
vii
10.4230/LIPIcs.TYPES.2011.i
article
Frontmatter, Table of Contents, Preface, Workshop Organization
Danielsson, Nils Anders
Nordström, Bengt
Frontmatter, Table of Contents, Preface, Workshop Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011.i/LIPIcs.TYPES.2011.i.pdf
Frontmatter
Table of Contents
Preface
Workshop Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
1
15
10.4230/LIPIcs.TYPES.2011.1
article
Non-constructive complex analysis in Coq
Brunel, Aloïs
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011.1/LIPIcs.TYPES.2011.1.pdf
Coq
winding number
complex analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
16
27
10.4230/LIPIcs.TYPES.2011.16
article
Infinitary Rewriting Coinductively
Endrullis, Jörg
Polonsky, Andrew
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011.16/LIPIcs.TYPES.2011.16.pdf
infinitary rewriting
coinduction
lambda calculus
standardization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
28
40
10.4230/LIPIcs.TYPES.2011.28
article
A new approach to the semantics of model diagrams
Granström, Johan G.
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011.28/LIPIcs.TYPES.2011.28.pdf
model diagram
modelling
metamodelling
semantics
compositionality
self-description
metacircularity
reflexivity
universal model
MOF
UML
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
41
54
10.4230/LIPIcs.TYPES.2011.41
article
Testing versus proving in climate impact research
Ionescu, Cezar
Jansson, Patrik
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011.41/LIPIcs.TYPES.2011.41.pdf
dependently-typed programming
domain-specific languages
climate impact research
formalization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-01-21
19
55
69
10.4230/LIPIcs.TYPES.2011.55
article
Verification of redecoration for infinite triangular matrices using coinduction
Matthes, Ralph
Picard, Celia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol019-types2011/LIPIcs.TYPES.2011.55/LIPIcs.TYPES.2011.55.pdf
nested datatype
coinduction
theorem proving
Coq