18th International Workshop on Types for Proofs and Programs (TYPES 2011), TYPES 2011, September 8-11, 2011, Bergen, Norway
TYPES 2011
September 8-11, 2011
Bergen, Norway
International Conference on Types for Proofs and Programs
TYPES
http://www.types.name/
https://dblp.org/db/conf/types
Leibniz International Proceedings in Informatics
LIPIcs
https://www.dagstuhl.de/dagpub/1868-8969
https://dblp.org/db/series/lipics
1868-8969
Nils Anders
Danielsson
Nils Anders Danielsson
Bengt
Nordström
Bengt Nordström
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
19
2013
978-3-939897-49-1
https://www.dagstuhl.de/dagpub/978-3-939897-49-1
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter
Table of Contents
Preface
Workshop Organization
i-vii
Front Matter
Nils Anders
Danielsson
Nils Anders Danielsson
Bengt
Nordström
Bengt Nordström
10.4230/LIPIcs.TYPES.2011.i
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Non-constructive complex analysis in Coq
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.
Coq
winding number
complex analysis
1-15
Regular Paper
Aloïs
Brunel
Aloïs Brunel
10.4230/LIPIcs.TYPES.2011.1
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Infinitary Rewriting Coinductively
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.
infinitary rewriting
coinduction
lambda calculus
standardization
16-27
Regular Paper
Jörg
Endrullis
Jörg Endrullis
Andrew
Polonsky
Andrew Polonsky
10.4230/LIPIcs.TYPES.2011.16
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
A new approach to the semantics of model diagrams
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.
model diagram
modelling
metamodelling
semantics
compositionality
self-description
metacircularity
reflexivity
universal model
MOF
UML
28-40
Regular Paper
Johan G.
Granström
Johan G. Granström
10.4230/LIPIcs.TYPES.2011.28
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Testing versus proving in climate impact research
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.
dependently-typed programming
domain-specific languages
climate impact research
formalization
41-54
Regular Paper
Cezar
Ionescu
Cezar Ionescu
Patrik
Jansson
Patrik Jansson
10.4230/LIPIcs.TYPES.2011.41
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode
Verification of redecoration for infinite triangular matrices using coinduction
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.
nested datatype
coinduction
theorem proving
Coq
55-69
Regular Paper
Ralph
Matthes
Ralph Matthes
Celia
Picard
Celia Picard
10.4230/LIPIcs.TYPES.2011.55
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode