Revues

This paper discusses research undertaken by the Curtin Open Knowledge Initiative (COKI) andparticipants during and following an Open Knowledge international workshop held in Mauritiusin September 2019. The workshop brought together key experts to explore the role of openknowledge in the creation of equitable and inclusive global knowledge landscapes. This paperexplores the role of open access and institutional repositories in knowledge sharing and thedissemination of research output from higher education and research institutions within theAfrican continent. The paper reviews the landscape of research output from the Africancontinent; analyses open access research output, overviews of institutional knowledge sharingpositions and the dissemination of research output from Ghana, Rwanda, South Africa andUganda.

Wilson, Katie

The combination of open access and our digital networked environment offers huge potential tomake the research outputs of humanities and social sciences more Findable, Accessible,Interoperable and Reusable (FAIR) and more easily available to the broader community for publicbenefit. Yet despite growing international policy derivatives, open digital scholarship hasencountered significant challenges. This study:• Reviewed key barriers currently hampering the uptake of these policies by diverse universityparticipants (senior university administrators, researchers, librarians, platform providers anddevelopers), policymakers and community users; and• Examined how these have influenced the fields of humanities and social sciences (HASS).This paper discusses research undertaken by the Curtin Open Knowledge Initiative (COKI) andparticipants during and following an Open Knowledge international workshop held in Mauritiusin September 2019. The workshop brought together key experts to explore the role of openknowledge in the creation of equitable and inclusive global knowledge landscapes. This paperexplores the role of open access and institutional repositories in knowledge sharing and thedissemination of research output from higher education and research institutions within theAfrican continent. The paper reviews the landscape of research output from the Africancontinent; analyses open access research output, overviews of institutional knowledge sharingpositions and the dissemination of research output from Ghana, Rwanda, South Africa andUganda.

Arthur, Paul

Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo a notion of equivalence based on the finite standard model. One main contribution of the paper is to establish that, somewhat surprisingly, the resulting notion of profinite lambda-term coming from Stone duality lives in perfect harmony with the principles of Reynolds parametricity. In addition, we show that the notion of profinite lambda-term is compositional by constructing a cartesian closed category of profinite lambda-terms, and we establish that the embedding from lambda-terms modulo beta-eta-conversion to profinite lambda-terms is faithful using Statman's finite completeness theorem. Finally, we prove that the traditional Church encoding of finite words into lambda-terms can be extended to profinite words, and leads to a homeomorphism between the space of profinite words and the space of profinite lambda-terms of the corresponding Church type.

van Gool, Sam

Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based process calculus that arises from the Curry-Howard interpretation of the intuitionistic semi-axiomatic sequent calculus and includes unrestricted recursion both at the level of types and processes. With our type refinement system, we can reason about the partial correctness of SAX programs, complementing prior work on sized type refinements that supports reasoning about termination. Our design regime synthesizes the infinitary proof theory of SAX with that of bidirectional typing and Hoare logic, deriving some standard reasoning principles for data and (co)recursion while enabling information hiding for codata. We prove syntactic type soundness, which entails a notion of partial correctness that respects codata encapsulation. We illustrate our language through a few simple examples.

Somayyajula, Siva