| 1. |
- Niemi, MEK, et al.
(författare)
-
- 2021
-
swepub:Mat__t
|
|
| 2. |
- Kanai, M, et al.
(författare)
-
- 2023
-
swepub:Mat__t
|
|
| 3. |
- Armstrong, Alasdair, et al.
(författare)
-
Kleene Algebra
- 2013
-
Ingår i: Archive of Formal Proofs. - 2150-914X.
-
Tidskriftsartikel (refereegranskat)
|
|
| 4. |
- Armstrong, Alasdair, et al.
(författare)
-
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
- 2013
-
Ingår i: Interactive Theorem Proving. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642396335 ; , s. 197-212
-
Konferensbidrag (refereegranskat)abstract
- Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while-programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.
|
|
| 5. |
- Armstrong, Alasdair, et al.
(författare)
-
Programming and automating mathematics in the Tarski-Kleene hierarchy
- 2014
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208. ; 83:2, s. 87-102
-
Tidskriftsartikel (refereegranskat)abstract
- We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how models can be programmed, including sets of traces and paths, languages, binary relations, max-plus and min-plus algebras, matrices, formal power series. For relation algebras we discuss primarily proof automation in a comprehensive library and present an advanced formalisation example.
|
|
| 6. |
- Jones, Benedict C, et al.
(författare)
-
To which world regions does the valence-dominance model of social perception apply?
- 2021
-
Ingår i: Nature Human Behaviour. - : Springer Science and Business Media LLC. - 2397-3374. ; 5:1, s. 159-169
-
Tidskriftsartikel (refereegranskat)abstract
- Over the past 10 years, Oosterhof and Todorov's valence-dominance model has emerged as the most prominent account of how people evaluate faces on social dimensions. In this model, two dimensions (valence and dominance) underpin social judgements of faces. Because this model has primarily been developed and tested in Western regions, it is unclear whether these findings apply to other regions. We addressed this question by replicating Oosterhof and Todorov's methodology across 11 world regions, 41 countries and 11,570 participants. When we used Oosterhof and Todorov's original analysis strategy, the valence-dominance model generalized across regions. When we used an alternative methodology to allow for correlated dimensions, we observed much less generalization. Collectively, these results suggest that, while the valence-dominance model generalizes very well across regions when dimensions are forced to be orthogonal, regional differences are revealed when we use different extraction methods and correlate and rotate the dimension reduction solution. PROTOCOL REGISTRATION: The stage 1 protocol for this Registered Report was accepted in principle on 5 November 2018. The protocol, as accepted by the journal, can be found at https://doi.org/10.6084/m9.figshare.7611443.v1 .
|
|
