| 21. |
- Abd Alrahman, Yehia, 1986, et al.
(author)
-
A coordination protocol language for power grid operation control
- 2019
-
In: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 109
-
Journal article (peer-reviewed)abstract
- Future power distribution grids will comprise a large number of components, each potentially able to carry out operations autonomously. Clearly, in order to ensure safe operation of the grid, individual operations must be coordinated among the different components. Since operation safety is a global property, modelling component coordination typically involves reasoning about systems at a global level. In this paper, we propose a language for specifying grid operation control protocols from a global point of view. In our model, operation control is yielded in communications driven by both the grid topology and by state-based information, features captured by novel language principles previously unexplored. We show how the global specifications can be used to automatically generate local controllers of individual components, and that the distributed implementation yielded by such controllers operationally corresponds to the global specification. We showcase our development by modelling a fault management scenario in power grids. (C) 2019 Elsevier Inc. All rights reserved.
|
|
| 22. |
- Abdollahi, Mehdi, 1985, et al.
(author)
-
Effect of stabilization method and freeze/thaw-aided precipitation on structural and functional properties of proteins recovered from brown seaweed (Saccharina latissima)
- 2019
-
In: Food Hydrocolloids. - : Elsevier BV. - 0268-005X. ; 96, s. 140-150
-
Journal article (peer-reviewed)abstract
- - Structural, functional and nutritional properties of protein recovered from brown seaweed, S. latissima with alkaline solubilization/isoelectric precipitation as a function of different post-harvest stabilization methods were studied. The latter included freezing at −20 °C/-80 °C, oven-drying, sun-drying, freeze-drying and ensilaging. Also, the efficacy of freeze/thaw-aided precipitation (F/T) in improving protein recovery of the process was evaluated. The freeze-dried, oven-dried, and −20 °C frozen seaweeds resulted in significantly higher protein yield than the −80°C-frozen, sun-dried and ensiled biomasses. F/T increased protein precipitation and doubled total protein yield. Sun-drying and −20°C-freezing caused extensive protein degradation as revealed by SDS-PAGE and HP-SEC, while oven-drying altered the seaweed protein structure with less α-helices. Functional properties of the seaweed proteins were remarkably affected by stabilization condition and F/T, but nutritional value of the proteins was only dependent on stabilization method. Thus, to efficiently recover seaweed proteins, its post-harvest stabilization condition must be carefully chosen based on the final application of the proteins. © 2019 The Authors
|
|
| 23. |
- Abdulwahhab, Sinan, 1991, et al.
(author)
-
The Role of Local Open Source Communities in the Development of Open Source Projects
- 2016
-
In: Open Source Systems: Integrating Communities, Oss 2016. - Berlin : Springer-Verlag Berlin. - 1868-4238 .- 1868-422X. - 9783319392257
-
Conference paper (peer-reviewed)abstract
- This paper investigates the position of local open source communities (LOSCs) in the development of open source projects (OSPs). We have conducted an empirical study to examine the role of LOSCs, their way of working, and the benefits/challenges they experience compared to the overall global community. The qualitative investigation consisted of ten semi-structured interviews with members within different LOSCs. The results confirm the importance of LOSCs and the pivotal role they play in the development of OSPs. In many cases, they act as the middleman between individual members and the project's global community. However, LOSCs have their own kinds of challenges.
|
|
| 24. |
- Abedin, Raschid, et al.
(author)
-
Topological Lie Bialgebras, Manin Triples and Their Classification Over g[[x]]
- 2024
-
In: Communications in Mathematical Physics. - 1432-0916 .- 0010-3616. ; 405:1
-
Journal article (peer-reviewed)abstract
- The main result of the paper is classification of topological Lie bialgebra structures on the Lie algebra g[[x]] , where g is a finite-dimensional simple Lie algebra over an algebraically closed field F of characteristic 0. We introduce the notion of a topological Manin pair (L,g[[x]]) and present their classification by relating them to trace extensions of F[[x]] . Then we recall the classification of topological doubles of Lie bialgebra structures on g[[x]] and view it as a special case of the classification of Manin pairs. The classification of topological doubles states that up to an appropriate equivalence there are only three non-trivial doubles. It is proven that topological Lie bialgebra structures on g[[x]] are in bijection with certain Lagrangian Lie subalgebras of the corresponding doubles. We then attach algebro-geometric data to such Lagrangian subalgebras and, in this way, obtain a classification of all topological Lie bialgebra structures with non-trivial doubles. For F= C the classification becomes explicit. Furthermore, this result enables us to classify formal solutions of the classical Yang–Baxter equation.
|
|
| 25. |
- Abedin, R., et al.
(author)
-
Topological Manin pairs and (n, s)-type series
- 2023
-
In: Letters in Mathematical Physics. - 0377-9017 .- 1573-0530. ; 113:3
-
Journal article (peer-reviewed)abstract
- Lie subalgebras of L = g((x)) x g[x]/x(n)g[x], complementary to the diagonal embedding Delta of g[x] and Lagrangian with respect to some particular form, are in bijection with formal classical r-matrices and topological Lie bialgebra structures on the Lie algebra of formal power series g[x]. In this work we consider arbitrary subspaces of L complementary to Delta and associate them with so-called series of type (n, s). We prove that Lagrangian subspaces are in bijection with skew-symmetric (n, s)-type series and topological quasi-Lie bialgebra structures on g[x]. Using the classificaiton of Manin pairs we classify up to twisting and coordinate transformations all quasi-Lie bialgebra structures. Series of type (n, s), solving the generalized classical Yang-Baxter equation, correspond to subalgebras of L. We discuss their possible utility in the theory of integrable systems.
|
|
| 26. |
- Abel, Andreas, 1974, et al.
(author)
-
A formalized proof of strong normalization for guarded recursive types
- 2014
-
In: Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319127354 ; 8858, s. 140-158
-
Conference paper (peer-reviewed)abstract
- We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep reduction is parametrized by a natural number “depth” that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.
|
|
| 27. |
- Abel, Andreas, 1974, et al.
(author)
-
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
- 2023
-
In: Proceedings of the ACM on Programming Languages. - 2475-1421. ; 7:ICFP, s. 920-954
-
Journal article (peer-reviewed)abstract
- We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has Pi-types, weak and strong Sigma-types, natural numbers, an empty type, and a universe, and we also extend the theory with a unit type and graded Sigma-types. The theory is parameterized by a modality, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable. The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped λ-calculus and removes erasable content, in particular function arguments with the "erasable"grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak Sigma-types.
|
|
| 28. |
|
|
| 29. |
- Abel, Andreas, 1974, et al.
(author)
-
Decidability of Conversion for Type Theory in Type Theory
- 2018
-
In: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 2:POPL, s. 23:1-23:29
-
Journal article (peer-reviewed)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.
|
|
| 30. |
- Abel, Andreas, 1974, et al.
(author)
-
Normalization by evaluation for call-by-push-value and polarized lambda calculus
- 2019
-
In: ACM International Conference Proceeding Series. - New York, NY, USA : ACM.
-
Conference paper (peer-reviewed)abstract
- We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on neutral terms of sum type. The placement of the monad influences the normal forms we obtain: for instance, placing the monad on coproducts gives us eta-long beta-pi normal forms where pi refers to permutation of case distinctions out of elimination positions. We further observe that placing the monad on every coproduct is rather wasteful, and an optimal placement of the monad can be determined by considering polarized simple types inspired by focalization. Polarization classifies types into positive and negative, and it is sufficient to place the monad at the embedding of positive types into negative ones. We consider two calculi based on polarized types: pure call-by-push-value (CBPV) and polarized lambda-calculus, the natural deduction calculus corresponding to focalized sequent calculus. For these two calculi, we present algorithms for normalization by evaluation. We further discuss different implementations of the monad and their relation to existing normalization proofs for lambda-calculus with sums. Our developments have been partially formalized in the Agda proof assistant.
|
|
