| 1. |
- Aronsson, Per, et al.
(författare)
-
An operational decision support tool for stump harvest
- 2011
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- A multi-criteria decision support tool was developed to optimise stump harvesting for energy in Sweden. The decision tool takes account of multiple, sometimes conflicting, criteria relating to stump harvest; energy and climate, economics, biodiversity, and soil and water. Data on harvested stems are used as primary input data in the tool. Such data are routinely collected in harvester computers. The tool effectively deals with mixed sets of data; quantitative harvest data are re-calculated to metric (e.g. stump biomass), and qualitative data (e.g. biodiversity implications) are incorporated. A digital terrain map derived from air-borne laser scanning provides basic data for estimating soil wetness, while digital maps of water courses, key habitats and protected areas, or other sensitive habitats, are used to identify potentially and practically harvestable stumps.In four sub-models, an index from 0 to 10 is calculated for each stump, with 0 representing ‘Not at all suitable’ and 10 ‘Highly suitable for extraction’. Through this, a stump of high value for wood-living species is assigned a low index in the biodiversity sub-model and a large, easily accessible stump is assigned a high index in the economic sub-model. When calculating the net index, the sub-indices can be weighted according to the preferences of the end-user.An energy and climate sub-model incorporates greenhouse gas (GHG) emissions from forest operations and the effect of advancing GHG emissions when stump biomass is incinerated instead of being left to decompose. In the economic sub-model the potential monetary return from each stump is calculated based on estimated revenue from harvested stump biomass and the costs of stump harvesting and forwarding operations (based on cost functions and GIS calculations of transport distances).The biodiversity sub-model considers four types of wood-dependent organisms (lichens, mosses, insects and fungi) in terms of their habitat requirements, vulnerability, sun exposure preferences, locality, etc. A panel of external experts has drawn up a grading scale of stump values for the different taxonomic groups. The proximity to key habitats and exposure to sunlight are derived from a spatial model.Soil and water issues are handled within a sub-model estimating the consequences for long-term soil fertility (nutrient cycling and soil compaction) and water (leaching of plant nutrients and mercury, and particle transport due to soil damage by heavy machinery).The tool offers the end-user possibilities to prioritise and plan for cost-effective stump harvesting, while minimising negative environmental impacts.
|
|
| 2. |
- LarsOlle, Anders, et al.
(författare)
-
A multi-criteria decision support model for optimal stump harvesting
- 2012
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- A multi-criteria decision support model for optimal stump harvesting Sweden was developed. The model quantifies the effect of harvesting each individual stump over a harvesting object in four criteria's: - Biodiversity (Biodiversity value index) - Economy (SEK) - Greenhouse gas emissions (CO2) - Soil and water (Soil and water preservation index) The four criteria's are sometimes in conflict to each other, and uses values that are not directly comparable. The intended use for this model is to contribute with the objective evaluation of all four criteria's in the decision in what stumps to harvest and what stumps to leave in the harvesting object. The model uses individual stump data (e.g. position, tree species and stump biomass) and harvesting object GIS data (roads, elevation map, soil map, terrain map). Primary data on individual stumps comes from the logging system in the stem harvesters: GPS and operator classification. Such data are routinely collected in harvesters. Official map data for the harvesting object are available from the Swedish mapping, cadastral and land registration authority (Lantmäteriet). This includes the topographic map and elevation maps data in 2 m resolution. Also, GIS data are collected in the inspections before harvesting the stems. The biodiversity sub-model considers different types of wood-dependent organisms (lichens, mosses, insects and fungi) in terms of their habitat requirements, vulnerability, sun exposure preferences, locality, etc. A panel of external experts has drawn up a grading scale of stump values for the different taxonomic groups. The proximity to key habitats and exposure to sunlight are derived from a spatial model. In the economic sub-model the potential net return from each stump is calculated based on estimated revenue from harvested stump biomass and the costs of stump harvesting and transport (based on cost functions and GIS calculations of transport distances). An energy and climate sub-model incorporates greenhouse gas (GHG) emissions from forest operations and the effect of advancing GHG emissions when stump biomass is incinerated instead of being left to decompose. Soil and water issues are handled within a sub-model estimating the consequences for long-term soil fertility (nutrient cycling and soil compaction) and water (leaching of plant nutrients and mercury, and particle transport due to soil damage by heavy machinery). Each criteria is evaluated in totally four sub-models. To be able to compare the resulting value from each of the criteria, a harvesting index from 0 to 1 is calculated for each stump. The value 0 represents ‘Not at all suitable for harvest’ and 1 ‘Highly suitable for harvest’. Through this, a stump of high biodiversity value is assigned a low harvesting index in the biodiversity sub-model and a large, easily accessible stump is assigned a high harvesting index in the economic sub-model. When calculating the total net index, the harvesting index from each criteria has to be weighed together using one coefficient for each criteria. The weighing coefficient for each criteria is chosen according to the preferences of the decision maker. The tool offers the end-user possibilities to prioritise and plan for cost-effective stump harvesting, while minimising negative environmental impacts.
|
|
| 3. |
- Ahrens, B., et al.
(författare)
-
From Signatures to Monads in UniMath
- 2019
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 285-318
-
Tidskriftsartikel (refereegranskat)abstract
- The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it-in particular, general inductive types are not part of the system. In this work, we partially remedy the lack of inductive types by constructing some set-level datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Lof type theory.
|
|
| 4. |
- Ahrens, Benedikt, et al.
(författare)
-
Implementing a category-theoretic framework for typed abstract syntax
- 2022
-
Ingår i: CPP '22. - New York : Association for Computing Machinery (ACM). - 9781450391825 ; , s. 307-323
-
Konferensbidrag (refereegranskat)abstract
- In previous work ("From signatures to monads in UniMath"),we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant.In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply-typed case. As it turns out, in many cases our mechanized results carried over to the generalized definitions without any code change. Second, an existing mechanized library on ?-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bicategorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using a recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly.The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation.
|
|
| 5. |
|
|
| 6. |
- Angiuli, Carlo, et al.
(författare)
-
Internalizing Representation Independence with Univalence
- 2021
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 5:POPL
-
Tidskriftsartikel (refereegranskat)abstract
- In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations.In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
|
|
| 7. |
- Brunerie, Guillaume, et al.
(författare)
-
Synthetic Integral Cohomology in Cubical Agda
- 2022
-
Ingår i: 30th EACSL Annual Conferenceon Computer Science Logic. - Saarbrücken/Wadern : Dagstuhl Publishing. - 9783959772181 ; , s. 11:1-11:19
-
Konferensbidrag (refereegranskat)abstract
- This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables signifcant simplifcations of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new defnition of the group structure for cohomology with Z-coefcients, optimized for efcient computations. We also invent an optimized defnition of the cup product which allows us to give the frst complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.
|
|
| 8. |
- Cano, G., et al.
(författare)
-
FORMALIZED LINEAR ALGEBRA OVER ELEMENTARY DIVISOR RINGS IN COQ
- 2016
-
Ingår i: Logical Methods in Computer Science. - : Centre pour la Communication Scientifique Directe (CCSD). - 1860-5974. ; 12:2
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents a COQ formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend Bezout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension <= 1 and well-founded strict divisibility.
|
|
| 9. |
- Cavallo, Evan, et al.
(författare)
-
Unifying Cubical Models of Univalent Type Theory
- 2020
-
Ingår i: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). - Saarbrücken/Wadern : Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH. - 9783959771320 ; , s. 14:1-14:17
-
Konferensbidrag (refereegranskat)abstract
- We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.
|
|
| 10. |
- Cohen, Cyril, 1985, et al.
(författare)
-
A Coq formalization of finitely presented modules
- 2014
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 8558, s. 193-208
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a formalization of constructive module theory in the intuitionistic type theory of Coq. We build an abstraction layer on top of matrix encodings, in order to represent finitely presented modules, and obtain clean definitions with short proofs justifying that it forms an abelian category. The goal is to use it as a first step to get certified programs for computing topological invariants, like homology groups and Betti numbers.
|
|
