| 1. |
|
|
| 2. |
- Coquand, Catarina, 1962
(författare)
-
A Formalised Proof of the Soundness and Completeness of Simply Typed Lambda Calculus with Explicit Substitution
- 2002
-
Ingår i: Higher-Order and Symbolic Computation. - 1573-0557 .- 1388-3690. ; 15:1, s. 57-90
-
Tidskriftsartikel (refereegranskat)abstract
- We present a simply-typed λ-calculus with explicit substitutions and we give a fully formalised proof of its soundness and completeness with respect to Kripke models. We further give conversion rules for the calculus and show also for them that they are sound and complete with respect to extensional equality in the Kripke model. A decision algorithm for conversion is given and proven correct. We use the technique "normalisation by evaluation" in order to prove these results, An important aspect of this work is that it is not a formalisation of an existing proof, instead the proof has been done in interaction with the proof system, ALF.
|
|
| 3. |
- Rompf, Tiark, et al.
(författare)
-
Scala-Virtualized : linguistic reuse for deep embeddings
- 2012
-
Ingår i: Higher-Order and Symbolic Computation. - : Springer Science and Business Media LLC. - 1388-3690 .- 2212-0793 .- 1573-0557. ; 25:1, s. 165-207
-
Tidskriftsartikel (refereegranskat)abstract
- Scala-Virtualized extends the Scala language to better support hosting embedded DSLs. Scala is an expressive language that provides a flexible syntax, type-level computation using implicits, and other features that facilitate the development of embedded DSLs. However, many of these features work well only for shallow embeddings, i.e. DSLs which are implemented as plain libraries. Shallow embeddings automatically profit from features of the host language through linguistic reuse: any DSL expression is just as a regular Scala expression. But in many cases, directly executing DSL programs within the host language is not enough and deep embeddings are needed, which reify DSL programs into a data structure representation that can be analyzed, optimized, or further translated. For deep embeddings, linguistic reuse is no longer automatic.Scala-Virtualized defines many of the language’s built-in constructs as method calls, which enables DSLs to redefine the built-in semantics using familiar language mechanisms like overloading and overriding. This in turn enables an easier progression from shallow to deep embeddings, as core language constructs such as conditionals or pattern matching can be redefined to build a reified representation of the operation itself.While this facility brings shallow, syntactic, reuse to deep embeddings, we also present examples of what we call deep linguistic reuse: combining shallow and deep components in a single DSL in such a way that certain features are fully implemented in the shallow embedding part and do not need to be reified at the deep embedding level.
|
|
| 4. |
- Salama, Cherif, et al.
(författare)
-
Static Consistency Checking for Verilog Wire Interconnects : Using dependent types to check the sanity of Verilog descriptions
- 2011
-
Ingår i: Higher-Order and Symbolic Computation. - New York, NY : Springer-Verlag New York. - 1388-3690 .- 2212-0793 .- 1573-0557. ; 24:1-2, s. 81-114
-
Tidskriftsartikel (refereegranskat)abstract
- The Verilog hardware description language has padding semantics that allow designers to write descriptions where wires of different bit widths can be interconnected. However, many of these connections are nothing more than bugs inadvertently introduced by the designer and often result in circuits that behave incorrectly or use more resources than required. A similar problem occurs when wires are incorrectly indexed by values (or ranges) that exceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the use of generate blocks to describe circuit families only makes the situation worse as it hides such inconsistencies making them harder to detect. Inconsistencies in the generated code are only exposed after elaboration when the code is fully-expanded.In this paper we show that these inconsistencies can be pinned down prior to elaboration using static analysis. We combine dependent types and constraint generation to reduce the problem of detecting the aforementioned inconsistencies to a satisfiability problem. Once reduced, the problem can easily be solved with a standard satisfiability modulo theories (SMT) solver. In addition, this technique allows us to detect unreachable code when it resides in a block guarded by an unsatisfiable set of constraints. To illustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with generative constructs and previously defined elaboration semantics. We prove that a well-typed FV description will always elaborate into an inconsistency-free description. We also provide a freely-available implementation demonstrating our approach. © 2011 Springer Science+Business Media, LLC.
|
|
| 5. |
- Jönsson, Mikael, et al.
(författare)
-
Glacial clay affects foraging performance in a Patagonian fish and cladoceran
- 2011
-
Ingår i: Hydrobiologia. - : Springer Science and Business Media LLC. - 0018-8158 .- 1573-5117. ; 663:1, s. 101-108
-
Tidskriftsartikel (refereegranskat)abstract
- Climate change is altering temperatures and precipitation patterns all over the world. In Patagonia, Argentina, predicted increase in precipitation together with rapidly melting glaciers increase the surface runoff, and thereby the transport of suspended solids to recipient lakes. Suspended solids affect the visual conditions in the water which in turn restricts visual foraging. The native fish Aplochiton zebra Jenyns, and its filter-feeding cladoceran prey, Daphnia commutata Ekman, were subjected to foraging experiments at three turbidity levels. A. zebra foraging rate was substantially reduced at naturally occurring turbidity levels and the filtering rate of D. commutata was reduced at the highest turbidity level. This indicates that Daphnia may be partly released from predation from A. zebra at the same time as it can maintain relatively high feeding rates as turbidity increases. Lower foraging rates at the same time as the metabolic demand increases, through increased temperatures, may result in larger effects on A. zebra than could be expected from increases in turbidity or temperature alone. Turbidity may, as an indirect effect of climate change, decrease planktivore foraging rates and thereby alter the interaction strength between trophic levels.
|
|
| 6. |
- Hamilos, Michalis, et al.
(författare)
-
Relationship between peripheral arterial reactive hyperemia and residual platelet reactivity after 600 mg clopidogrel
- 2011
-
Ingår i: Journal of Thrombosis and Thrombolysis. - : Springer Science and Business Media LLC. - 0929-5305 .- 1573-742X. ; 32:1, s. 64-71
-
Tidskriftsartikel (refereegranskat)abstract
- Clopidogrel reduces long-term ischemic events in patients with acute coronary syndrome or stable angina (SA) undergoing percutaneous coronary intervention (PCI). Endothelial function improvement has been proposed, among other factors, for this beneficial effect of clopidogrel, but whether this might be associated to its anti-platelet action remains unclear. We tested the hypothesis that clopidogrel improvement of peripheral vascular endothelial function might be associated with inhibition of platelet aggregation. Endothelial function was evaluated before and at least 12 h after 600 mg clopidogrel in 43 SA pts undergoing elective PCI by: (a) reactive hyperemia peripheral arterial tonometry (measuring the Endoscore); (b) circulating endothelial microparticles (EMPs). Response to clopidogrel was measured with point-of-care VerifyNow P2Y12 assay and expressed as platelet reaction unit (PRU) and percent platelet inhibition (%PI). High platelet reactivity after clopidogrel was defined as PRU ≥ 240. Endothelial function improved after clopidogrel in 20 pts. Changes in Endoscore (Δ Endoscore) were significantly correlated with both PRU (r = -0.61, P < 0.001) and %PI (r = 0.57, P < 0.001). Endoscore significantly increased after clopidogrel in pts with PRU < 240 (0.38 ± 0.26 to 0.57 ± 0.33, P < 0.001), but did not in pts with PRU ≥ 240 (0.53 ± 0.31 to 0.40 ± 0.37, P = 0.12). EMPs were also significantly reduced in pts with PRU < 240 (222 [140-593] to 142 [83-371]/μl, P = 0.001), while no changes were observed in pts with PRU ≥ 240 (256 [178-531] to 388 [238-499]/μl, P = 0.55). In patients with stable coronary artery disease, a single 600 mg clopidogrel loading dose improves vascular endothelial function. This improvement is associated with optimal platelet inhibition and it is not observed in patients with post-clopidogrel high platelet reactivity.
|
|
| 7. |
- Holfve-Sabel, Mary-Anne
(författare)
-
Learning, interaction and relationships as components of student well-being : differences between classes from student and teacher perspective
- 2014
-
Ingår i: Social Indicators Research. - : Springer. - 0303-8300 .- 1573-0921. ; 119:3, s. 1535-1555
-
Tidskriftsartikel (refereegranskat)abstract
- The attitudes of students to their school, teachers and peers were investigated with 1,540 students in grade six from 30 schools and 78 classes. Using structural equation modelling, the students’ perceptions of well-being were investigated at class level using seven items with high reliability. Their well-being was dependent on at least three factors: students’ learning (seven items), student-to-student interaction (six items) and teacher–student relationships as described by students (ten items). Together, these factors explained 72 % of the variability of well-being between classes. The students’ well-being appeared to be significantly different between schools and between classes in the same school. The teachers’ opinions of their classes with the highest class score for well-being were compared with the lowest. The differences in the evaluation of the teachers’ own classes explain a number of critical issues which impact on educational outcomes. Students need to be aware of the combined effects of learning and socialisation.
|
|
| 8. |
- Vilejshikova, E. V., et al.
(författare)
-
Luminescence of Eu:Y3Al5O12, Eu:Lu3Al5O12, and Eu:GdAlO3 Nanocrystals Synthesized by Solution Combustion
- 2017
-
Ingår i: Journal of Applied Spectroscopy. - : Springer-Verlag New York. - 0021-9037 .- 1573-8647. ; 84:5, s. 866-874
-
Tidskriftsartikel (refereegranskat)abstract
- Nanocrystals of rare-earth garnets Y3Al5O12 and Lu3Al5O12 and perovskite GdAlO3 highly doped (10–20 at%) with Eu3+ are synthesized by the solution combustion technique and subsequent annealing in air at 800 and 1300oC. Their structure, morphology, and phase composition are studied. These materials exhibit intense red luminescence under UV excitation. Eu:GdAlO3 luminescence has CIE 1931 color coordinates (0.632, 0.368); dominant wavelength, 599.6 nm; and color purity, >99%. Judd–Ofelt parameters, luminescence branching ratios, and lifetimes of the Eu3+ 5D0 state are determined. The luminescence quantum yield for Eu:GdAlO3 (10 at%) reaches 74% with a lifetime of 1.4 ms for the 5D0 state. The synthesized materials are promising for red ceramic phosphors.
|
|
