Abstract

Abstract
Strategic term rewriting and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies (recursion schemes) to apply term rewrite rules in defining transformations, while the latter is suitable for expressing context-dependent language processing algorithms. Each of these techniques, however, is usually implemented by its own powerful and large processor system. As a result, it makes such systems harder to extend and to combine. We present the embedding of both strategic tree rewriting and attribute grammars in a zipper-based, purely functional setting. The embedding of the two techniques in the same setting has several advantages: First, we easily combine/zip attribute grammars and strategies, thus providing language engineers the best of the two worlds. Second, the combined embedding is easier to maintain and extend since it is written in a concise and uniform setting. We show the expressive power of our library in optimizing Haskell let expressions, expressing several Haskell refactorings and solving several language processing tasks for an Oberon-0 compiler.

Abstract
Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt.

Abstract
Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user's trust, which is the process of generating a random password. We present three of the most commonly used algorithms and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt to specify and verify our reference implementation. In addition, we present a proof-of-concept prototype that extends Bitwarden to only generate compliant passwords, solving a frequent users' frustration with PMs. This demonstrates that our formally verified component can be integrated into an existing (and widely used) PM.

Abstract

Abstract
The paper presents the work carried out at the HCI Engineering Education workshop, organised by IFIP working groups 2.7/13.4 and 13.1. It describes four case studies of projects and exercises used in Human-Computer Interaction Engineering courses. We propose a common framework for presenting the case studies and describe the four case studies in detail. We then draw conclusions on the differences between the presented case studies that highlight the diversity and multidisciplinary aspects to be taught in a Human-Computer Interaction Engineering course. As future work, we plan to create a repository of case studies as a resource for teachers.