The ACP Seminar usually takes place on Mondays from 14:15 to 15:00. ACP members can schedule a talk by sending speaker, title, abstract, and scheduling preferences to Matteo Acclavio. Ph.D. students can be awarded ECTS when partaking in the seminar.
Judith Kankam-Boateng | IMADA meeting room 4 | video meeting
Small and medium-sized enterprises (SMEs) in defence supply chains face growing cybersecurity threats but lack the resources to respond effectively. This paper examines the cybersecurity perceptions of three stakeholder groups in Denmark’s defence supply chain: policymakers (PM), policy promoters (PP), and policy implementers (PI). Through focus group discussions with 45 participants — 6 PMs, 11 PPs, and 28 PIs (representatives from 12 SMEs) — we investigate how each group perceives cybersecurity and what organisational vulnerabilities and capabilities these perceptions reveal. Our analysis identifies 45 vulnerabilities across five categories, but only 17 capabilities, resulting in a pronounced imbalance at the SME level. Policymakers frame cybersecurity as a strate- gic national concern, SMEs experience it as a compliance burden, and policy promoters lack sufficient reach to bridge this gap. Applying a vulnerability–capability lens, we identify a capability translation problem. National-level assets, including centralised incident management and international partnerships, do not cascade to the SMEs they are designed to support. We offer differentiated recommendations for each stakeholder group and for designing targeted awareness programmes that account for divergent mental models across the supply chain.
Stefano Volpe | IMADA meeting room 4
(This talk is an encore of my 2026/03/09 presentation. This time, I will focus on the PL semantics side, and not assume familiarity with category theory nor coalgebras.) The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin’s original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching.
Sandra Greiner | IMADA meeting room 4 | video meeting
Refactoring service-oriented software is crucial for competitiveness, security, and reliability. While the migration of monoliths to (micro-)services is well-studied, the evolution of a service-oriented architecture – particularly, the integration of API patterns – falls short, leaving practitioners with little knowledge on the impact of architectural refactorings. In this talk, we will use and study an existing framework for applying refactorings either internally in the refactored service(s), adjacently (in the same application but another service component), or externally in a remote service. I will show the results of studying the impact on performance as observed on the client side of these implementation variants. Lastly, I will outline research directions on how to extend and build on our work.
Stefano Volpe | IMADA meeting room 4 | video meeting
The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin’s original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching.
Robin Kaarsgaard Sales | IMADA meeting room 4 | video meeting
Quantum computing improves substantially on known classical algorithms for various important problems, but the nature of the relationship between quantum and classical computing is not yet fully understood. This relationship can be clarified by free models, that add to classical computing just enough physical principles to represent quantum computing and no more. In this talk, I will describe an axiomatisation of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one. The axioms and model are based on reversible classical computing, isolate quantum advantage in the ability to take certain well-behaved square roots, and link to various quantum computing hardware platforms. This approach allows combinatorial optimisation, including brute force computer search, to optimise quantum computations. The free model may be interpreted as a programming language for quantum computers, that has the same expressivity and computational universality as the standard model, but additionally allows automated verification and reasoning.
Bjarke Paluszewski (Sandra Greiner's M.Sc. student) | IMADA meeting room 3 | video meeting
Rust is a modern language that guarantees memory-safety while supporting low-level concepts similar to C and C++. Particularly, it has a built-in feature-expression language and allows for configuring the usage of Rust crates (libraries) used in other Rust projects. Yet the variability in the Rust ecosystem remains largely undiscovered leaving developers confronted with several issues such as including too many unnecessary features, feature versioning, and possible feature interactions. In our talk, we demonstrate how to analyze the variability inherent in single Rust crates. We show how a feature model can be synthesized by different Rust configurations (selection of features of a used Rust library in another Rust project) using an FCA based method. We analyze the resulting feature models to understand the size of the configuration space and the usage of features among Rust libraries.
Malthe Petersen (Dan Plyukhin's M.Sc. student) | IMADA meeting room 4 | video meeting
Davide Taibi (SDU Veijle) | IMADA meeting room 4 | video meeting
What if the future of software architecture doesn't need architects as we know them? As GenAI infiltrates every stage of the software development lifecycle, the traditional role of the architect—meticulously designing systems from requirements to deployment—is being unbundled, redefined, and partially outsourced to machines. And yet, the industry is far from ready. This keynote presents a bold vision of the AI-Augmented Architect: a hybrid thinker who doesn't write blueprints alone but designs with AI, using it not as a tool—but as a creative partner, a challenger, a simulator of trade-offs. Drawing from two cutting-edge empirical studies, including a multivocal review of GenAI in software architecture and a forward-looking survey of industry leaders, we'll confront hard truths: AI is already doing architectural documentation, detecting antipatterns, and even suggesting design alternatives. But it's also hallucinating, biasing decisions, and eroding accountability. If we don't rethink our roles, methods, and mindset, software architects risk becoming passive validators of AI output rather than strategic designers of complex systems. The good news? There is still time to adapt—but only if we embrace a future where architecture is not less human, but more profoundly human because of our collaboration with machines.
Judith Kankam-Boateng | IMADA meeting room 4
(1) Cybersecurity Insights Gleaned from World Religions by Karen Renaud and Marc Dupuis. Abstract: Despite security policies and training, employees continue to make mistakes that trigger cybersecurity incidents. This paper explores an unconventional source of insight: world religions, which have millennia of experience accommodating human frailties. We interviewed religious leaders and reviewed religious literature to develop a 'vision for cybersecurity' that was then evaluated by cybersecurity professionals. Our goal is to launch debate around more equitable best practices that better account for human nature. (2) "Even after two years, we still have a bad feeling": Two Comparative Case Studies of the Effects of a Cyberattack on Fear, Trust in the IT Department and Security-Related Stress by Markus Schöps, Sangavi Shanthakumar, and M. Angela Sasse. Abstract: Cyberattacks can have lasting psychological effects on employees and their relationship with IT departments. We studied two research organizations—one breached, one not—using questionnaires (n=149) and interviews with IT staff (n=8). Employees at the breached organization reported less trust in IT, worse communication, and more security-related stress. We found that stricter post-attack security measures, though well-intentioned, may paradoxically decrease employee trust and increase stress for everyone. (3) 'There was a bit of PTSD every time I walked through the office door': Ransomware harms and the factors that influence the victim organization's experience by Gareth Mott, Sarah Turner, Jason R.C. Nurse, et al. Abstract: Ransomware inflicts wide-ranging harms beyond financial losses. Through interviews and workshops with 83 professionals (including victims, responders, and law enforcement), we identify severe organizational impacts—business interruption, reputation damage—and under-reported employee harms including acute psychological and physical effects. We also identify factors that moderate these harms, such as preparedness and leadership culture. Our findings position ransomware as a whole-of-organization crisis, not merely an "IT problem."
Siddharth Bhaskar | IMADA meeting room 4
The predominant design philosophy behind most Discrete Mathematics (DM) courses is that of a recycling bin: a place where mathematical prerequisites with no other natural home can live out the rest of their days in peace. This fundamentally misunderstands the role of mathematics in computer science. Instead of being a collection of topical prerequisites, mathematics provides a conceptual framework enabling the sort of high-level computational thinking that a computer science bachelor's degree is supposed to train. I argue that the field of mathematics in question can be profitably identified with elementary set theory, roughly, the theory of (naive) sets and relations with structural induction. I propose an alternate model of mathematics education in the computer science degree: a `DM1' (and possibly DM2) course that receives as much importance as the CS1/2 sequence and are similarly foregrounded in the program of study.
Giorgia Sampó | IMADA meeting room 4
"What we talk about when we talk about DAOs": Decentralized Autonomous Organizations (DAOs) integrate blockchain-based automation with novel forms of collective governance, yet research on them remains fragmented across technical and organizational silos, hindering a comprehensive understanding of DAOs as socio-technical systems. To bridge these gaps, we first conduct a systematic umbrella review of 12 prior surveys to map research themes and persistent gaps. Based on this analysis, we propose a novel, three-layer framework that explicitly links (i) technical artefacts (the infrastructure, e.g., tokens, smart contracts), (ii) governance logics (the rules, e.g., incentives, consensus mechanisms), and (iii) organizational manifestations (the outcomes, e.g., proposals, votes). By making cross-layer dependencies explicit, the framework enables more holistic theorizing, supports comparative empirical work, and provides a diagnostic tool for practitioners dealing with design trade-offs between decentralization, efficiency, and participation. "Pathways to Performance: A Configurational Analysis of Consensus in DAOs": Decentralized Autonomous Organizations (DAOs) represent a radical form of socio-technical systems, where rules are enforced by code and governance is conducted by a distributed network of stakeholders. A critical challenge in designing these systems is achieving consensus without centralized authority, yet how consensus ensures effective governance remains underexplored. This study investigates the design of DAO governance systems, utilizing data from 70 DAOs and applying Fuzzy Set Qualitative Comparative Analysis (fsQCA) to explore which consensus configurations lead to positive organizational outcomes. Our analysis challenges the notion of a single consensus model. Instead, we uncover 13 distinct configurations that characterize successful DAOs. Our key finding reveals a fundamental “ideation/legitimation trade-off”: successful DAOs optimize for broad participation in either the proposal (ideation) stage or the voting (legitimation) stage, but rarely both. These insights provide a nuanced framework for understanding and designing effective governance systems for DAOs.
Judith Kankam-Boateng | IMADA meeting room 4
Small and medium-sized enterprises (SMEs) are facing growing cybersecurity threats amidst limited resources and regulatory complexity. This complexity stems from diverse stakeholders in the regulatory process, ranging from policy makers to industry associations to the companies having to implement the regulations. Misalignments between these different stakeholders can further compound the complexity. Against this backdrop, we investigate the cybersecurity mental models held by three stakeholder groups in Denmark’s defence sector and how they might influence regulatory processes. Using a qualitative approach that combines focus groups with 6 policymakers, 11 policy promoters (industry associations), and 12 policy implementers (SMEs), we reveal key misalignments in perceptions of risk, threats, cyber readiness, and policy interpretation. Our findings further show that SMEs often treat cybersecurity as a compliance task, while policy makers assume strategic readiness. From our results, we suggest recommendations for aligning governance frameworks with organisational realities.
Fabrizio Montesi | IMADA meeting room 4
A few years ago, some researchers at SDU got interested in mechanizing a couple of things using the Rocq (née Coq) proof assistant. In the most outrageous example of scope creep of all time, Fabrizio is now trying to formalize every single thing anyone has ever said (now using Lean instead of Rocq). And for 45 minutes this Monday, he'll tell us about it!
Robin Kaarsgaard Sales | IMADA meeting room 4
A central pursuit in quantum computing is to identify the minimal resources required to achieve universality. Within the quantum circuit model, this is studied by considering the gate sets that provide the fundamental instructions from which quantum algorithms are built. However, standard gate sets such as Clifford+T contain some instructions that are disproportionately powerful, obscuring the precise source of quantum computational power. While single-gate universal sets are known, these rely on rotation angles that are irrational multiples of 2pi , requiring fine-tuned control that is difficult to achieve on quantum hardware today. Here, we show the surprising result that the controlled-V (or controlled-sqrt(X)) gate, a simple two-qubit interaction previously described as "semi-classical" and already widely used in reversible logic synthesis and directly realisable on leading hardware platforms, suffices on its own to perform universal quantum computation. Our construction, based on catalytic embedding and a procedure to generate the necessary resource states, simulates standard universal gate sets with constant overhead, highlighting how the full power of quantum computation can emerge from unexpectedly simple ingredients.
Judith Kankam-Boateng | IMADA meeting room 4
Small and medium-sized enterprises (SMEs) are facing growing cybersecurity threats amidst limited resources and regulatory complexity. This complexity stems from diverse stakeholders in the regulatory process, ranging from policy makers to industry associations to the companies having to implement the regulations. Misalignments between these different stakeholders can further compound the complexity. Against this backdrop, we investigate the cybersecurity mental models held by three stakeholder groups in Denmark’s defence sector and how they might influence regulatory processes. Using a qualitative approach that combines focus groups with 6 policymakers, 11 policy promoters (industry associations), and 12 policy implementers (SMEs), we reveal key misalignments in perceptions of risk, threats, cyber readiness, and policy interpretation. Our findings further show that SMEs often treat cybersecurity as a compliance task, while policy makers assume strategic readiness. From our results, we suggest recommendations for aligning governance frameworks with organisational realities.
Casper Bach | IMADA meeting room 4
Reduction-based interpreters are traditionally defined in terms of a one-step reduction function which systematically decomposes a term into a potential redex and context, contracts the redex, and recomposes it to construct the new term to be further reduced. While implementing such interpreters follows a systematic recipe, they often require interpreter engineers to write a substantial amount of code—much of it boilerplate. In this paper, we apply well-known techniques from generic programming to reduce boilerplate code in reduction-based interpreters.
Siddharth Bhaskar | IMADA meeting room 4
In any monotone inductive definition, we repeatedly add elements to a set until we achieve a fixed point. The stage of an element in the fixed point is the first ordinal where it appears in this process. A theory of monotone inductive definitions enjoys the stage comparison property in case the query comparing elements by their stages in a definable induction, is itself definable. The proof that positive elementary induction satisfies this property is basically a functional transforming the original induction into a definition of the corresponding stage comparison query. It is tricky and short application of higher-order reasoning. Sufficiently abstracted, I think it could qualify as a "functional pearl." I would like to present the theorem and see if you agree! My secret hope is to prove a plausible strengthening of this property that is natural and plausible but has baffled me for years.
Viktor Strate Kløvedal | IMADA meeting room 4
Alessio Pellegrino | IMADA meeting room 4
Given a combinatorial optimisation problem, there are typically multiple ways of modelling it for presentation to an automated solver. Choosing the right combination of model and target solver can have a significant impact on the effectiveness of the solving process. The best combination of model and solver can also be instance-dependent: there may not exist a single combination that works best for all instances of the same problem. We consider the task of building machine learning models to automatically select the best combination for a problem instance. Critical to the learning process is to define instance features, which serve as input to the selection model. Our contribution is the automatic learning of instance features directly from the high-level representation of a problem instance using a transformer encoder. We evaluate the performance of our approach using the Essence modelling language via a case study of three problem classes.
Xueying Qin | IMADA meeting room 4
Judith Kankam-Boateng | IMADA meeting room 4
This study investigates how scenario-based simulations transform cybersecurity practices among Danish SMEs. Focus group discussions were conducted before and after exposure to threat scenarios. Results demonstrate significant shifts in awareness, particularly regarding supply chain vulnerabilities, cloud service risks, and geopolitical factors. Participants evolved from fragmented, reactive approaches toward structured responsibility mapping and proactive risk assessment. Communication strategies transitioned from informal exchanges to formalized practices with leadership involvement. The findings reveal that experiential learning effectively expands threat perception beyond technical issues to encompass organizational culture and human factors.
Mako Bates (University of Vermont) | IMADA meeting room 4
Choreographic programming (CP) is a paradigm for implementing distributed systems that uses a single global program to define the actions and interactions of all participants. Library-level CP implementations, like HasChor, integrate well with mainstream programming languages but have several limitations: Their conditionals require extra communication; they require specific host-language features (e.g., monads); and they lack support for programming patterns that are essential for implementing realistic distributed applications. We make three contributions to library-level CP to specifically address these challenges. First, we propose and formalize conclaves and multiply-located values, which enable efficient conditionals in library-level CP without redundant communication. Second, we propose end-point projection as dependency injection, a design pattern that enables library-level CP in host languages without support for monads. Third, we propose census polymorphism, a technique for abstracting over the number of participants in a choreography. We demonstrate these contributions via implementations in Haskell, Rust, and TypeScript.
Luc Edixhoven (SDU) | IMADA meeting room 4
Extraction of choreographies is a way to mechanically obtain a choreography from a given network of processes. A recent paper by Luís, Kim, Fabrizio and Larisa presented a state of the art extraction methodology. They proved its soundness (i.e., 'any extracted choreography is good'), but not completeness (i.e., 'it always works'). Fabrizio and I are now trying to prove this, but it turns out to be tricky. In this talk, I will sketch our progress so far, up to the latest wall we hit (at least at the moment of writing this abstract). As this is work in progress, it will be structured only up to a point, and be mostly on a board. Input is much welcome!
Siddharth Bhaskar | IMADA meeting room 4
Why does the s in dogs sound like a z? Phonology is that branch of linguistics that explains the relationship between words (the things stored in our head) and their pronunciations (the acoustics that we produce when we say them). In this talk, I will explain how programming language theory sheds light on two problems in phonology. One concerns classes of subregular functions, which are string-to-string transformations computed by finite state machines. The other concerns building a type theory for phonology as a whole. This is an extended version of my “IMADA speaks” talk, but one where I actually get to the problems and say something about their solutions. It should be quite accessible, and I hope that it brings a new angle to some familiar concepts!
Pietro Ferrara (University of Venice) | IMADA meeting room 4
Modern software architectures comprise several programming languages, frameworks, technologies, and structures. While most existing software comprises several distinct distributed components, how the software is organized and how the different components communicate depends on the specific architectural style adopted. In addition, software architectures evolved quickly: multi-tier (typically front-end, back-end, and database), service-oriented, microservices, and serverless architectures are a few examples of widely adopted architectures. However, some common patterns can be identified. In particular, distinct nodes of the distributed system usually communicate either synchronously through REST APIs or asynchronously through pub/sub messaging. This allows us to abstract together implementations using different technological solutions. Nevertheless, applying sound static analysis to such a diversified technological ecosystem remains challenging. Defining the semantics, proving the soundness of abstractions, and implementing the analyses require ad hoc approaches for each pattern. In this talk, we will present the current trends we experienced in modern software architectures and how we approached the sound static analysis of such software.
Matteo Trentin | IMADA meeting room 4
Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the scheduling (e.g., re- source allocation, runtime environments) of stateless functions. Recent work proposed using domain-specific languages to express per-function policies, e.g., policies that enforce the allocation on nodes that enjoy lower latencies to databases and services used by the function. Here, we focus on affinity-aware scenarios, i.e., where, for performance and functional requirements, the allocation of a function depends on the presence/absence of other functions on nodes. We present aAPP, an extension of a declarative, platform- agnostic language that captures affinity-aware scheduling at the FaaS level. We implement an aAPP-based prototype on Apache OpenWhisk. Besides proving that a FaaS platform can capture affinity awareness using aAPP and improve performance in affinity-aware scenarios, we use our prototype to show that aAPP imposes no noticeable overhead in scenarios without affinity constraints.
Stelios Tsampas | IMADA meeting room 4
Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of a variable store fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, which guarantees that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin's powerful theory of Mathematical Operational Semantics (abstract GSOS) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to reconcile abstract GSOS with imperative semantics have thus failed. We propose a novel approach to the operational semantics of imperative languages based on the formal distinction between readers (terms that act on an initial input store), and writers (running terms that have already been provided an initial store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques for free. We demonstrate that our approach generates non-trivial compositionality results for imperative languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence.
Giulia Manara | IMADA meeting room 4
We introduce a novel approach to studying properties of processes in the pi-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free pi-calculus. Our method provides a simple logical characterisation of deadlock freedom for the recursion- and race-free fragment of the pi-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite pi-calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the computation-as-derivation paradigm extends the reach of logical methods for the study of concurrency, by bridging gaps between logic, the expressiveness of the pi-calculus, and the expressiveness of choreographic languages.
Robin Kaarsgaard Sales | IMADA meeting room 4
We introduce a programming language that is computationally universal for reversible quantum computing. It extends the universal classical reversible programming language Π with a single primitive corresponding to the Hadamard gate. The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory, enabling reasoning about the equivalence of quantum programs in a way that can be automated. The completeness is proven by means of a novel finite presentation of the groups of orthogonal matrices with entries in the ring Z[1/√2].
Christian Grube Hviid Nesting (Dan's M.Sc. student) | IMADA meeting room 4
Choreographic programming is a paradigm for writing distributed applications with strong static guarantees. Choreographic programs must explicitly define "where" computation happens and "how" data is moved. Being explicit this way is useful for writing high-performance code, but it also means prototyping choreographic programs can be tedious. To enable rapid prototyping, we developed a tool for the Choral choreographic programming language that automatically inserts missing communications. This talk will introduce Choral, explain the tool's user interface and implementation, and present interesting technical challenges for future work.
Xueying Qin | IMADA meeting room 4
In this talk, I will provide an overview of several projects I completed during my PhD, as well as the project I have been working on since joining SDU. Specifically, I will discuss three past projects that explore topics in programming languages, including formal specifications and implementations, monolithic and distributed programs, and the semantics of syntactic transformations: (1) Primrose: Selecting Container Data Types by Their Properties, (2) Panopticon: A Universal Method Invocation Library for Rust, (3) Shoggoth: A Formal Foundation for Strategic Rewriting. Finally, I will present my current project: Mechanising a Choreographic Language in Lean 4.
Magnus Madsen and students (Aarhus University) | IMADA meeting room 4
"Associated Effects: Flexible Abstractions for Effectful Programming". We present associated effects, a programming language feature that enables type classes to abstract over the effects of their function signatures, allowing each type class instance to specify its concrete effects. Associated effects significantly increase the flexibility and expressive power of a programming language that combines a type and effect system with type classes. In particular, associated effects allow us to (i) abstract over total and partial functions, where partial functions may throw exceptions, (ii) abstract over immutable data structures and mutable data structures that have heap effects, and (iii) implement adaptors that combine type classes with algebraic effects. We implement associated effects as an extension of the Flix programming language and refactor the Flix Standard Library to use associated effects, significantly increasing its flexibility and expressive power. Specifically, we add associated effects to 11 type classes, which enables us to add 28 new type class instances. "Restrictable Variants: A Simple and Practical Alternative to Extensible Variants". We propose restrictable variants as a simple and practical alternative to extensible variants. Restrictable variants combine nominal and structural typing: a restrictable variant is an algebraic data type indexed by a type-level set formula that captures its set of active labels. We introduce new pattern-matching constructs that allows programmers to write functions that only match on a subset of variants, i.e., pattern-matches may be non-exhaustive. We then present a type system for restrictable variants which ensures that such non-exhaustive matches cannot get stuck at runtime. An essential feature of restrictable variants is that the type system can capture structure-preserving transformations: specifically the introduction and elimination of variants. This property is important for writing reusable functions, yet many row-based extensible variant systems lack it. In this paper, we present a calculus with restrictable variants, two partial pattern-matching constructs, and a type system that ensures progress and preservation. The type system extends Hindley-Milner with restrictable variants and supports type inference with an extension of Algorithm W with Boolean unification. We implement restrictable variants as an extension of the Flix programming language and conduct a few case studies to illustrate their practical usefulness. Relational nullable types with Boolean unification We present a simple, practical, and expressive relational nullable type system. A relational nullable type system captures whether an expression may evaluate to null based on its type, but also based on the type of other related expressions. The type system extends the Hindley-Milner type system with Boolean constraints, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support full Hindley-Milner style type inference with an extension of Algorithm W. We conduct a preliminary study of open source projects showing that there is a need for relational nullable type systems across a wide range of programming languages. The most important findings from the study are: (i) programmers use programming patterns where the nullability of one expression depends on the nullability of other related expressions, (ii) such invariants are commonly enforced with run-time exceptions, and (iii) reasoning about these programming patterns requires not only knowledge of when an expression may evaluate to null, but also when it may evaluate to a non-null value. We incorporate these observations in the design of the proposed relational nullable type system.
Casper Bach | IMADA meeting room 4
Automated program transformation tools should ideally come with correctness guarantees that they preserve well-boundness and well-typedness. However, tools that provide such guarantees are rare in practice. A challenge for giving such guarantees is the lack of a clear binding model for languages with non-lexical binding such as modules, classes, etc. In this talk I'll present an approach to building and verifying type-safe refactorings for languages with non-lexical binding. The approach consists of a type and scope discipline, inspired by previous work on scope graphs. We demonstrate the discipline on a module calculus, and discuss how the discipline lets us implement and verify renamings and refactorings that preserve well-boundness and well-typedness.
Sandra Greiner and Marco Chiarandini (IMADA) | IMADA meeting room 4
Finding the perfect solution to complex problems, like the traveling salesman or the knapsack problem, is mostly computationally infeasible. Optimization algorithms have been developed to compute optimal solutions efficiently. Randomized optimization heuristics (ROHs) are a special class of such algorithms to compute close to optimal solutions. They contain components that use random and heuristic choices, often inspired by natural phenomena. Compared to their deterministic counterparts, ROHs tend to be simpler to design and implement while offering improved performance, particularly on large problems whose internal structure is not sufficiently well known or even available. However, randomized optimization algorithms are still far from reaching the level of widespread and systematic adoption enjoyed by more traditional optimization solvers in the real world. One reason being that in practice they must be redesigned and implemented anew for every problem. However, while the kind of problems and, thus, the solving algorithms are different and come with different properties, they also share some foundational commonalities, like trying to construct solutions for problems, exploring the neighborhood of solutions, and following the guidance of one or multiple optimization objectives. In an EU Cost Action, we work towards specifying a common specification that allows for modeling different types of problems uniformly and to deploy different solutions algorithms easily. A particular aim of this specification is to support different programming languages and paradigms to be generated from the instantiated model. In our talk, we introduce the concept of randomized optimization heuristics and an initial draft of a specification. The specification should support users in specifying the problem and corresponding solutions. Contrary to a mathematical formalization, this modeling approach aims at easily deriving an implementation in a specific target language. Particular challenges arise from trying to not restrict the specification to a particular programming paradigm (functional vs procedural vs object-oriented) or a specific target language. Furthermore, ROHs rely on probing different solutions for a problem by exploring a neighborhood. While one solution can be computed and effectively used, others may be just assessed but not used. Thus, elements of concurrency may play a role when developing such a specification, a point we would like to discuss in our talk.
Giorgia Sampó | IMADA meeting room 4
Decentralized Autonomous Organizations (DAOs) denote an emerging organizational phenomenon that builds heavily on technologies and concepts in computer science. Despite growing interest in DAOs, however, research has yet to thoroughly explore the exchange of knowledge across these two disciplines, particularly in terms of the nature, scale, and direction of these interactions. Using bibliometric methods and citation networks to map interdisciplinary knowledge flows, this study focuses on how the fields borrow ideas and methodologies from each other, employ them, and contribute to a common pool of knowledge. By drawing a parallelism with Digital Humanities we show how the academic conversation about DAOs would deeply benefit from such an analysis. Gathering a deeper understanding of where and how emerging knowledge was created has in fact provided scholars with means to foster active collaboration among disciplines, identify contact areas, and gather and share the expertise needed for the field to progress. Moreover, analysing the content and shape of these knowledge exchanges is vital to identifying feasible strategies to support theoretical and critical forms of interdisciplinarity, able to go beyond the simple borrowing of methods and concepts to instrumentally apply from one field to the other. Our findings highlighted mutual exchanges among the fields, characterized by a majority of interactions taking place through boundary (or common) papers, confirming the existence of an interdisciplinary conversation. Furthermore, the analysis of the dominant pattern of interdisciplinary interaction confirmed the importance of boundary papers, where most of the connections took place, and pointed towards the emergence of a new community revolving around DAOs. By combining these results with a topic modeling analysis on interaction networks we also proved that most of the conversations take the form of case studies and applications, thus suggesting a lack of theoretically oriented exchanges in favor of functional and instrumental ones. Shedding light on these processes, this paper aims at gathering a better understanding of the existing conversation, to be used by future researchers to foster a flourishing exchange and to build novel theoretical frameworks and approaches, as well as new interdisciplinary theories and perspectives.
Marco Prandini (University of Bologna / SDU) | IMADA meeting room 4
Software-defined networking and network function virtualization have brought unparalleled flexibility in defining and managing network architectures. With the widespread diffusion of cloud platforms, more resources are available to execute virtual network functions concurrently, but the current approach to defining networks in the cloud development is held back by the lack of tools to manage the composition of more complex flows than simple sequential invocations. In this paper, we advocate for the usage of choreographic programming for defining the multiparty workflows of a network. When applied to the composition of virtual network functions, this approach yields multiple advantages: (1) a single program expresses the behavior of all components, in a way that is easier to understand and check; (2) a compiler can produce the executable code for each component, guaranteeing correctness properties of their interactions such as deadlock freedom; (3) the bottleneck of a central orchestrator is removed. We describe the proposed approach and show its feasibility via a case study where different functions cooperatively solve a security monitoring task.
Nina Berger (TU Darmstadt) | IMADA meeting room 4
This talk will explore the social dimensions of security and privacy to enhance user engagement and behaviors in these areas. A core focus of my research is the role of informal, social interactions in enhancing cybersecurity awareness and resilience. By studying peer-to-peer support and barriers to effective S&P assistance, I seek to identify strategies to facilitate meaningful, informal conversations that promote security and privacy knowledge among users. I also focus on the complexities of privacy negotiation in Internet of Things (IoT)-equipped environments, particularly in shared spaces. Through interviews, surveys, and workshops, I have uncovered significant misalignments in privacy expectations between IoT owners and their guests, underscoring the need for transparent and socially sensitive design interventions. The talk will also address the impact of gender stereotypes in the S&P field, revealing how stereotypical media portrayals affect women’s engagement with security topics. Finally, my work addresses challenges in digital consent, proposing enhanced consent interfaces and Personal Information Management Systems (PIMS) that better communicate data tracking implications to users. By providing clarity and meaningful engagement opportunities, these tools aim to improve users’ informed decision-making abilities.
Simon Daniel (TU Darmstadt) | IMADA meeting room 4
The field of parallel and distributed systems has been established for decades and the relevance of communication in the context of programming is still growing. With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. In traditional programming languages, application developers must ensure that communication between nodes is correct and free of deadlocks. Multiparty and choreographic languages, address these issues by combining the code for all actors in a single specification. This approach facilitates reasoning about distributed behaviour and promises inherent guarantees of deadlock freedom. Functional programming is a paradigm that clearly separates pure mathematical functions from side-effectful code. Recently, a practical implementation of a functional choreographic programming library has been published in Haskell. This paper builds upon the choreographic concept in the functional programming language Lean by adding features and increasing the safety of distributed value access.
Sandra Greiner | IMADA meeting room 4