| 1. |
- Abdulla, Parosh A., et al.
(författare)
-
Well Structured Transition Systems with History
- 2015
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; :193, s. 115-128
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a formal model of concurrent systems in which the history of a computation is explicitly represented as a collection of events that provide a view of a sequence of configurations. In our model events generated by transitions become part of the system configurations leading to operational semantics with historical data. This model allows us to formalize what is usually done in symbolic verification algorithms. Indeed, search algorithms often use meta-information, e.g., names of fired transitions, selected processes, etc., to reconstruct (error) traces from symbolic state exploration. The other interesting point of the proposed model is related to a possible new application of the theory of well-structured transition systems (wsts). In our setting wsts theory can be applied to formally extend the class of properties that can be verified using coverability to take into consideration (ordered and unordered) historical data. This can be done by using different types of representation of collections of events and by combining them with wsts by using closure properties of well-quasi orderings.
|
|
| 2. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types
- 2014
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - 2075-2180.
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms. The normalizer consists of two coinductively defined functions in the delay monad: One is a standard evaluator of lambda terms to closures, the other a type-directed reifier from values to h-long b-normal forms. Their composition, normalization-by-evaluation, is shown to be a total function a posteriori, using a standard logical-relations argument. The successful formalization serves as a proof-of-concept for coinductive programming and reasoning using sized types and copatterns, a new and presently experimental feature of Agda.
|
|
| 3. |
- Adams, Robin, 1978
(författare)
-
QPEL: Quantum Program and Effect Language
- 2014
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; 172, s. 133-153
-
Konferensbidrag (refereegranskat)abstract
- We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that allows semantics in terms of Hilbert spaces, C*-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Who is to blame? – Runtime verification of distributed objects with active monitors
- 2019
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - 2075-2180. ; 302, s. 32-46
-
Konferensbidrag (refereegranskat)abstract
- Since distributed software systems are ubiquitous, their correct functioning is crucially important. Static verification is possible in principle, but requires high expertise and effort which is not feasible in many eco-systems. Runtime verification can serve as a lean alternative, where monitoring mechanisms are automatically generated from property specifications, to check compliance at runtime. This paper contributes a practical solution for powerful and flexible runtime verification of distributed, object-oriented applications, via a combination of the runtime verification tool LARVA and the active object framework PROACTIVE. Even if LARVA supports in itself only the generation of local, sequential monitors, we empower LARVA for distributed monitoring by connecting monitors with active objects, turning them into active, communicating monitors. We discuss how this allows for a variety of monitoring architectures. Further, we show how property specifications, and thereby the generated monitors, provide a model that splits the blame between the local object and its environment. While LARVA itself focuses on monitoring of control-oriented properties, we use the LARVA front-end STARVOORS to also capture data-oriented (pre/post) properties in the distributed monitoring. We demonstrate this approach to distributed runtime verification with a case study, a distributed key/value store.
|
|
| 5. |
- Artho, Cyrille, et al.
(författare)
-
Model-based Testing of the Java network API
- 2017
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - : OPEN PUBL ASSOC. - 2075-2180. ; :245, s. 46-51
-
Tidskriftsartikel (refereegranskat)abstract
- Testing networked systems is challenging. The client or server side cannot be tested by itself. We present a solution using tool "Modbat" that generates test cases for Java's network library java.nio, where we test both blocking and non-blocking network functions. Our test model can dynamically simulate actions in multiple worker and client threads, thanks to a carefully orchestrated design that covers non-determinism while ensuring progress.
|
|
| 6. |
- Bartoletti, Massimo, et al.
(författare)
-
Preface
- 2016
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - : OPEN PUBL ASSOC. - 2075-2180. ; :223
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 7. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Assessing the Unitary RNN as an End-to-End Compositional Model of Syntax
- 2022
-
Ingår i: EPTCS 366. Proceedings End-to-End Compositional Models of Vector-Based Semantics, NUI Galway, 15-16 August, 2022, edited by: Michael Moortgat and Gijs Wijnholds. - Waterloo, Australia : Open Publishing Association. - 2075-2180.
-
Konferensbidrag (refereegranskat)abstract
- We show that both an LSTM and a unitary-evolution recurrent neural network (URN) can achieve encouraging accuracy on two types of syntactic patterns: context-free long distance agreement, and mildly context-sensitive cross serial dependencies. This work extends recent experiments on deeply nested context-free long distance dependencies, with similar results. URNs differ from LSTMs in that they avoid non-linear activation functions, and they apply matrix multiplication to word embeddings encoded as unitary matrices. This permits them to retain all information in the processing of an input string over arbitrary distances. It also causes them to satisfy strict compositionality. URNs constitute a significant advance in the search for explainable models in deep learning applied to NLP.
|
|
| 8. |
- Curzi, Gianluca, 1991
(författare)
-
Linear Additives
- 2021
-
Ingår i: Electronic Proceedings in Theoretical Computer Science (EPTCS). - 2075-2180.
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: typable terms of LAM enjoy linear strong normalization. Moreover, a mildly weakened version of cut-elimination for this system is proven which takes a cubic number of steps. Finally, we define a sound translation from LAM’s proofs into IMLL2’s linear lambda terms, and we study its complexity.
|
|
| 9. |
|
|
| 10. |
- Gurov, Dilian, et al.
(författare)
-
Self-Correlation and Maximum Independence in Finite Relations
- 2015
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; :191, s. 60-74
-
Tidskriftsartikel (refereegranskat)abstract
- We consider relations with no order on their attributes as in Database Theory. An independent partition of the set of attributes S of a finite relation R is any partition (sic) of S such that the join of the projections of R over the elements of (sic) yields R. Identifying independent partitions has many applications and corresponds conceptually to revealing orthogonality between sets of dimensions in multidimensional point spaces. A subset of S is termed self-correlated if there is a value of each of its attributes such that no tuple of R contains all those values. This paper uncovers a connection between independence and self-correlation, showing that the maximum independent partition is the least fixed point of a certain inflationary transformer alpha that operates on the finite lattice of partitions of S. alpha is defined via the minimal self-correlated subsets of S. We use some additional properties of alpha to show the said fixed point is still the limit of the standard approximation sequence, just as in Kleene's well-known fixed point theorem for continuous functions.
|
|
