| 1. |
- Abarenkov, Kessy, et al.
(författare)
-
Annotating public fungal ITS sequences from the built environment according to the MIxS-Built Environment standard – a report from a May 23-24, 2016 workshop (Gothenburg, Sweden)
- 2016
-
Ingår i: MycoKeys. - : Pensoft Publishers. - 1314-4057 .- 1314-4049. ; 16, s. 1-15
-
Tidskriftsartikel (refereegranskat)abstract
- Recent molecular studies have identified substantial fungal diversity in indoor environments. Fungi and fungal particles have been linked to a range of potentially unwanted effects in the built environment, including asthma, decay of building materials, and food spoilage. The study of the built mycobiome is hampered by a number of constraints, one of which is the poor state of the metadata annotation of fungal DNA sequences from the built environment in public databases. In order to enable precise interrogation of such data – for example, “retrieve all fungal sequences recovered from bathrooms” – a workshop was organized at the University of Gothenburg (May 23-24, 2016) to annotate public fungal barcode (ITS) sequences according to the MIxS-Built Environment annotation standard (http://gensc.org/mixs/). The 36 participants assembled a total of 45,488 data points from the published literature, including the addition of 8,430 instances of countries of collection from a total of 83 countries, 5,801 instances of building types, and 3,876 instances of surface-air contaminants. The results were implemented in the UNITE database for molecular identification of fungi (http://unite.ut.ee) and were shared with other online resources. Data obtained from human/animal pathogenic fungi will furthermore be verified on culture based metadata for subsequent inclusion in the ISHAM-ITS database (http://its.mycologylab.org).
|
|
| 2. |
- Abel, Andreas, 1974, et al.
(författare)
-
Decidability of Conversion for Type Theory in Type Theory
- 2018
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 2:POPL, s. 23:1-23:29
-
Tidskriftsartikel (refereegranskat)abstract
- Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-Löf Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.
|
|
| 3. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by evaluation for sized dependent types
- 2017
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 1:ICFP
-
Tidskriftsartikel (refereegranskat)abstract
- Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics. In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier (\forall) which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Î for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.
|
|
| 4. |
- Abel, Andreas, 1974, et al.
(författare)
-
Well-founded recursion with copatterns and sized types
- 2016
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 0956-7968 .- 1469-7653. ; 26
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non determinism and does not rely on coverage. Since System F-omega is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.
|
|
| 5. |
- Ackerley, Rochelle, 1980, et al.
(författare)
-
Case Studies in Neuroscience: Sensations elicited and discrimination ability from nerve cuff stimulation in an amputee over time
- 2018
-
Ingår i: Journal of Neurophysiology. - : American Physiological Society. - 0022-3077 .- 1522-1598. ; 120:1, s. 291-295
-
Tidskriftsartikel (refereegranskat)abstract
- The present case study details sensations elicited by electrical stimulation of peripheral nerve axons using an implanted nerve cuff electrode, in a participant with a transhumeral amputation. The participant uses an osseointegrated electromechanical interface, which enables skeletal attachment of the prosthesis and long-term, stable, bidirectional communication between the implanted electrodes and prosthetic arm. We focused on evoking somatosensory percepts, where we tracked and quantified the evolution of perceived sensations in the missing hand. which were evoked from electrical stimulation of the nerve, for over 2 yr. These sensations included small, pointlike areas of either vibration or pushing, to larger sensations over wider areas, indicating the recruitment of a few and many afferents, respectively. Furthermore, we used a two-alternative forced choice paradigm to measure the level of discrimination between trains of brief electrical stimuli, to gauge what the participant could reliably distinguish between. At best, the participant was able to distinguish a 05-Hz difference and on average acquired a 3.8-Hz just-noticeable difference at a more stringent psychophysical level. The current work shows the feasibility for long-term sensory feedback in prostheses, via electrical axonal stimulation, where small and relatively stable percepts were felt that may be used to deliver graded sensory feedback. This opens up opportunities for signaling feedback during movements (e.g., for precision grip), but also for conveying more complex cutaneous sensations. such as texture. NEW & NOTEWORTHY We demonstrate the long-term stability and generation of sensations from electrical peripheral nerve stimulation in an amputee. through an osseointegrated implant. We find that perceived tactilelike sensations could be generated for over 2 yr. in the missing hand. This is useful for prosthetic development and the implementation of feedback in artificial body parts.
|
|
| 6. |
- Adalbjornsson, S. I., et al.
(författare)
-
Estimating Periodicities in Symbolic Sequences Using Sparse Modeling
- 2015
-
Ingår i: Ieee Transactions on Signal Processing. - : Institute of Electrical and Electronics Engineers (IEEE). - 1053-587X .- 1941-0476. ; 63:8, s. 2142-2150
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we propose a method for estimating statistical periodicities in symbolic sequences. Different from other common approaches used for the estimation of periodicities of sequences of arbitrary, finite, symbol sets, that often map the symbolic sequence to a numerical representation, we here exploit a likelihood-based formulation in a sparse modeling framework to represent the periodic behavior of the sequence. The resulting criterion includes a restriction on the cardinality of the solution; two approximate solutions are suggested-one greedy and one using an iterative convex relaxation strategy to ease the cardinality restriction. The performance of the proposed methods are illustrated using both simulated and real DNA data, showing a notable performance gain as compared to other common estimators.
|
|
| 7. |
- Adawi, Tom, 1970, et al.
(författare)
-
Characterizing Software Engineering Students' Discussions during Peer Instruction : Opportunities for Learning and Implications for Teaching
- 2016
-
Ingår i: International Journal of Engineering Education. - 0949-149X. ; 32:2, s. 927-936
-
Tidskriftsartikel (refereegranskat)abstract
- Peer instruction is a method for activating students during lectures, which has gained a considerable amount of attention in higher education due to claims of dramatic improvement in learning gains. The purpose of this qualitative research study is to investigate what types of discussions engineering students engage in during a peer instruction session and what learning possibilities that are enabled by these different types of discussions. We observed twelve students during six separate and simulated peer instruction sessions and the students were interviewed individually after the sessions.Ananalysis of the data revealed that the students engaged in three qualitatively different types of discussions: affirmative discussions, motivating discussions, and argumentative discussions. We characterize these different types of discussions in terms of the number of alternative answers the students discuss, the extent to which they draw on prior knowledge and experiences, as well as the fundamental difference between an explanation and an argument. A good opportunity for learning is opened up when students are aspiring to find the truth, not simply being satisfied with what they believe to be true. We conclude that students do not always engage in discussions that support their learning in the best way, and we discuss implications for using peer instruction as a teaching method.
|
|
| 8. |
- Adermark, Louise, 1974, et al.
(författare)
-
Age-contingent influence over accumbal neurotransmission and the locomotor stimulatory response to acute and repeated administration of nicotine in Wistar rats
- 2015
-
Ingår i: Neuropharmacology. - : Elsevier BV. - 0028-3908. ; 97, s. 104-112
-
Tidskriftsartikel (refereegranskat)abstract
- Nicotine addiction is one of the leading contributors to the global burden of disease, and early onset smokers report a more severe addiction with lower chance of cessation than those with a late onset. Preclinical research supports an age-dependent component to the rewarding and reinforcing properties of nicotine, and the aim of this study was to. define behavioral adaptations and changes in accumbal neurotransmission that arise over 15 days of intermittent nicotine treatment (0.36 mg/kg/day) in rats of three different ages (5 weeks, 10 weeks, 36 weeks old). Repeated treatment increased the locomotor stimulatory response to nicotine in all age groups, but significantly faster in the two younger groups. In addition, nicotine decreased rearing activity in a way that sustained even after repeated administration in aged rats but not in the younger age groups. Electrophysiological field potential recordings revealed a decline in input/output function in the nucleus accumbens (NAc) of animals intermittently treated with nicotine starting at 5 weeks of age, but not in older animals. In drug naive rats, acute administration of nicotine modulated both accumbal dopamine output and excitatory transmission in a partially age dependent manner. Fifteen days of intermittent nicotine treatment did not alter the acute effect displayed by nicotine on dopamine levels or evoked field potentials. The data presented here show that both acute and repeated nicotine administration modulates accumbal neurotransmission and behavior in an age-contingent manner and that these age-dependent differences could reflect important neurobiological underpinnings associated with the increased vulnerability for nicotine-addiction in adolescents. (C) 2015 Elsevier Ltd. All rights reserved.
|
|
| 9. |
- Afzal, Wasif, et al.
(författare)
-
Software Test Process Improvement Approaches: A Systematic Literature Review and an Industrial Case Study
- 2016
-
Ingår i: Journal of Systems and Software. - : Elsevier BV. - 0164-1212. ; 111, s. 1-33
-
Tidskriftsartikel (refereegranskat)abstract
- Software Test Process Improvement (STPI) approaches are frameworks that guide software development organizations to improve their software testing process. We have identified existing STPI approaches and their characteristics (such as completeness of development, availability of information and assessment instruments, and domain limitations of the approaches) using a systematic literature review (SLR). Furthermore, two selected approaches (TPI Next and TMMi) are evaluated with respect to their content and assessment results in industry. As a result of this study, we have identified 18 STPI approaches and their characteristics. A detailed comparison of the content of TPI Next and TMMi is done. We found that many of the STPI approaches do not provide sufficient information or the approaches do not include assessment instruments. This makes it difficult to apply many approaches in industry. Greater similarities were found between TPI Next and TMMi and fewer differences. We conclude that numerous STPI approaches are available but not all are generally applicable for industry. One major difference between available approaches is their model representation. Even though the applied approaches generally show strong similarities, differences in the assessment results arise due to their different model representations.
|
|
| 10. |
- Ageborg Morsing, Julia, et al.
(författare)
-
Wind Turbine Noise and Sleep: Pilot Studies on the Influence of Noise Characteristics
- 2018
-
Ingår i: International Journal of Environmental Research and Public Health. - : MDPI AG. - 1661-7827 .- 1660-4601. ; 15:11
-
Tidskriftsartikel (refereegranskat)abstract
- The number of onshore wind turbines in Europe has greatly increased over recent years, a trend which can be expected to continue. However, the effects of wind turbine noise on long-term health outcomes for residents living near wind farms is largely unknown, although sleep disturbance may be a cause for particular concern. Presented here are two pilot studies with the aim of examining the acoustical properties of wind turbine noise that might be of special relevance regarding effects on sleep. In both pilots, six participants spent five consecutive nights in a sound environment laboratory. During three of the nights, participants were exposed to wind turbine noise with variations in sound pressure level, amplitude modulation strength and frequency, spectral content, turbine rotational frequency and beating behaviour. The impact of noise on sleep was measured using polysomnography and questionnaires. During nights with wind turbine noise there was more frequent awakening, less deep sleep, less continuous N2 sleep and increased subjective disturbance compared to control nights. The findings indicated that amplitude modulation strength, spectral frequency and the presence of strong beats might be of particular importance for adverse sleep effects. The findings will be used in the development of experimental exposures for use in future, larger studies.
|
|
