bluuebunny/crossref_metadata_2025_split huggingface dataset:
Green‐Solvent‐Processable Composite Micro/Nanofiber Membrane with Gradient Asymmetric Structure for Efficient Microfiltration
Authors: Ji Keyu , Liu Chengkun , He Haijun , Mao Xue , Wei Liang , Zhou Fenglei , Sun Runjun 
Published: April 2023

AbstractElectrospinning technology has attracted extensive attention in recent decades and is widely used to prepare nanofiber membranes from hundreds of polymers. Polyvinyl formal acetal (PVFA), as a polymer with excellent properties such as high strength and heat resistance, is not reported on the electrospun water treatment membrane. In this paper, the preparation process of electrospun PVFA nanofiber membrane is optimized, and the effect of sodium chloride (NaCl) addition on the physical and mechanical properties and microfiltration performance of nanofiber membrane is also explored. And the hydrophobic PVFA nanofiber filter layer is then combined with a hydrophilic nonwoven support layer to construct a composite micro/nanofiber membrane with a pore‐size gradient structure and a hydrophilic/hydrophobic asymmetric structure. Finally, unidirectional water transport and water treatment performance are further investigated. The results show that the tensile breaking strength of the composite membrane can reach up to 37.8 MPa, the retention rate for particles with the size of 0.1–0.3 µm is 99.7%, and the water flux is 513.4 L m−2h−1under the hydrostatic pressure. Moreover, it still has a retention of more than 98% after three repeated uses. Therefore, the electrospun PVFA composite membrane has a great potential in microfiltration.
Introduction: African American Environmental Knowledge at Niagara
Authors: Klestil Matthias 
Published: April 2023

AbstractTo define the concept of environmental knowledge and illustrate its potential for ecocritical readings of nineteenth-century African American literature, this chapter turns to two texts about Niagara Falls, a handwritten note by Frederick Douglass (1843) and Charles W. Chesnutt’s short story “The Passing of Grandison” (1899). While Douglass’s note exemplifies how black writers could transform dominant aesthetic modes such as the sublime to utter social critique through expressing epistemological and ethical relations to non-human nature, Chesnutt’s story demonstrates a strategic subversiveness characteristic of African American environmental knowledge. My readings highlight howEnvironmental Knowledge, Race, and African American Literatureemploys a Foucauldian ecocritical concept of environmental knowledge to trace places and patterns of an African American ecoliterary tradition.
Euroscapes: Space, Place, and Multi-Level Governance in European Television Crime Series
Authors: Dobrescu Caius , Waade Anne Marit 
Published: April 2023

AbstractIn this chapter, we present a theoretical framework for analysing the interaction between European governance models and the representational policies of places in crime narratives. We adopt a pan-European perspective that implies not only the broad diversity of the considered national examples, but first and foremost covers the points of intersection between different layers of territorial jurisdiction. In our mapping of European crime series we follow, while slightly adapting, the interfaces of four distinct scales and contexts considered by Hooghe and Marks (2001a, b). The chapter does not argue for the aggregation of all European crime series into a homogeneous storyworld, but rather attempts to monitor their location on a conceptual map of European governance.
Confronting Memories: The Case of Babylon Berlin
Authors: Coviello Massimiliano 
Published: April 2023

AbstractBabylon Berlin (2017–present), based on the novels by Volker Kutscher, was distributed by Sky and Netflix across Europe and globally. Set during the Weimar Republic (1918–1933), the German European TV series follows the life and investigations of Commissioner Gereon Rath, a man traumatized by his experience during World War I. This chapter addresses creative, production-related, stylistic, and narrative elements of Babylon Berlin. The series’ recreation of Weimar-era Berlin allows it to examine the lasting effects of the collective historical traumas experienced by Germany and Europe during the interwar period. More specifically, Babylon Berlin becomes a cultural and symbolic space that facilitates a reflection not only on the legacy of past traumas, but also on the connections between early twentieth-century Europe and the present.
Logics for Extensional, Locally Complete Analysis via Domain Refinements
Authors: Ascari Flavio , Bruni Roberto , Gori Roberta 
Published: April 2023

AbstractAbstract interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness Logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple $$\vdash _{A}[P]~\textsf{c}~[Q]$$

⊢
A

[
P
]

c

[
Q
]

in the logic implies completeness of an intensional abstraction of program $$\textsf{c}$$
c
on input P and is such that Q can be used to decide (in)correctness. However, completeness itself is an extensional property of the function computed by the program, while the above intensional analysis depends on the way the program is written and therefore not all valid triples can be derived in the proof system. Our main contribution is the study of new inference rules which allow one to perform part of the intensional analysis in a more precise abstract domain, and then to transfer the result back to the coarser domain. With these new rules, all (extensionally) valid triples can be derived in the proof system, thus untying the set of provable properties from the way the program is written.
Interpreting Knowledge-based Programs
Authors: Knapp Alexander , Mühlberger Heribert , Reus Bernhard 
Published: April 2023

AbstractKnowledge-based programs specify multi-agent protocols with epistemic guards that abstract from how agents learn and record facts or information about other agents and the environment. Their interpretation involves a non-monotone mutual dependency between the evaluation of epistemic guards over the reachable states and the derivation of the reachable states depending on the evaluation of epistemic guards. We apply the technique of a must/cannot analysis invented for synchronous programming languages to the interpretation problem of knowledge-based programs and demonstrate that the resulting constructive interpretation is monotone and has a least fixed point. We relate our approach with existing interpretation schemes for both synchronous and asynchronous programs. Finally, we describe an implementation of the constructive interpretation and illustrate the procedure by several examples and an application to the Java memory model.
Contextual Modal Type Theory with Polymorphic Contexts
Authors: Murase Yuito , Nishiwaki Yuichi , Igarashi Atsushi 
Published: April 2023

AbstractModal types—types that are derived from proof systems of modal logic—have been studied as theoretical foundations of metaprogramming, where program code is manipulated as first-class values. In modal type systems, modality corresponds to a type constructor for code types and controls free variables and their types in code values. Nanevski et al. have proposed contextual modal type theory, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by contexts—the types of all free variables in code values.This paper presents $$\lambda _{\forall []}$$

λ

∀
[
]

, a novel extension of contextual modal type theory with parametric polymorphism over contexts. Such an extension has been studied in the literature but, unlike earlier proposals, $$\lambda _{\forall []}$$

λ

∀
[
]

is more general in that it allows multiple occurrence of context variables in a single context. We formalize $$\lambda _{\forall []}$$

λ

∀
[
]

with its type system and operational semantics given by $$\beta $$
β
-reduction and prove its basic properties including subject reduction, strong normalization, and confluence. Moreover, to demonstrate the expressive power of polymorphic contexts, we show a type-preserving embedding from a two-level fragment of Davies’ $$\lambda _{\bigcirc }$$

λ
◯

, which is based on linear-time temporal logic, to $$\lambda _{\forall []}$$

λ

∀
[
]

.
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Authors: Kappé Tobias , Schmid Todd , Silva Alexandra 
Published: April 2023

AbstractGuarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa’s axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT consisting of skip-free programs.
Quorum Tree Abstractions of Consensus Protocols
Authors: Cirisci Berk , Enea Constantin , Mutluergil Suha Orhun 
Published: April 2023

AbstractDistributed algorithms solving agreement problems like consensus or state machine replication are essential components of modern fault-tolerant distributed services. They are also notoriously hard to understand and reason about. Their complexity stems from the different assumptions on the environment they operate with, i.e., process or network link failures, Byzantine failures etc. In this paper, we propose a novel abstract representation of the dynamics of such protocols which focuses on quorums of responses (votes) to a request (proposal) that form during a run of the protocol. We show that focusing on such quorums, a run of a protocol can be viewed as working over a tree structure where different branches represent different possible outcomes of the protocol, the goal being to stabilize on the choice of a fixed branch. This abstraction resembles the description of recent protocols used in Blockchain infrastructures, e.g., the protocol supporting Bitcoin or Hotstuff. We show that this abstraction supports reasoning about the safety of various algorithms, e.g., Paxos, PBFT, Raft, and HotStuff, in a uniform way. In general, it provides a novel induction based argument for proving that such protocols are safe.
MAG$$\pi $$: Types for Failure-Prone Communication
Authors: Le Brun Matthew Alan , Dardha Ornela 
Published: April 2023

AbstractMultiparty Session Types(MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network,e.g., assuming TCP-based communication where messages are guaranteed to be delivered; or adopting centralised reliable nodes and ad-hoc notions of reliability; or only addressing a single kind of failure, such as node crashes. In this work, we develop MAG$$\pi $$π—a Multiparty, Asynchronous and Generalised$$\pi $$π-calculus, which is thefirst language and type systemto accommodate in unison: (i) the widest range of non-Byzantine faults, includingmessage loss, delaysandreordering;crashandlink failures; andnetwork partitioning; (ii) a novel and most general notion ofreliability, taking into account the viewpoint ofeachparticipant in the protocol; (iii) a spectrum of network assumptions from the lowest UDP-based network programming to the TCP-based application level. We prove subject reduction and session fidelity; process properties (deadlock freedom, termination,etc.); failure-handling safety and reliability adherence.
System $$F^\mu _\omega $$ with Context-free Session Types
Authors: Poças Diogo , Costa Diana , Mordido Andreia , Vasconcelos Vasco T. 
Published: April 2023

AbstractWe study increasingly expressive type systems, from$$F^\mu $$Fμ—an extension of the polymorphic lambda calculus with equirecursive types—to$$F^{\mu ;}_\omega $$Fωμ;—the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of$$F^\mu _\omega $$Fωμas studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes.
Bunched Fuzz: Sensitivity for Vector Metrics
Authors: wunder june , Amorim Arthur Azevedo de , Baillot Patrick , Gaboardi Marco 
Published: April 2023

AbstractProgram sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum.In this work, we show that these products can be generalized to arbitrary $$L^p$$

L
p

distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases $$L^1$$

L
1

and $$L^\infty $$

L
∞

. To ease the handling of such products, we extend the Fuzz type system with bunches—as in the logic of bunched implications—where the distances of different groups of variables can be combined using different $$L^p$$

L
p

distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs.
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
Authors: Khajwal Basim , Ong C.-H. Luke , Wagner Dominik 
Published: April 2023

AbstractWe study the foundations of variational inference, which frames posterior inference as an optimisation problem, for probabilistic programming. The dominant approach for optimisation in practice is stochastic gradient descent. In particular, a variant using the so-called reparameterisation gradient estimator exhibits fast convergence in a traditional statistics setting. Unfortunately, discontinuities, which are readily expressible in programming languages, can compromise the correctness of this approach. We consider a simple (higher-order, probabilistic) programming language with conditionals, and we endow our language with both a measurable and asmoothed(approximate) value semantics. We present type systems which establish technical pre-conditions. Thus we can prove stochastic gradient descent with the reparameterisation gradient estimator to be correct when applied to the smoothed problem. Besides, we can solve the original problem up to any error tolerance by choosing an accuracy coefficient suitably. Empirically we demonstrate that our approach has a similar convergence as a key competitor, but is simpler, faster, and attains orders of magnitude reduction in work-normalised variance.
Type-safe Quantum Programming in Idris
Authors: Dandy Liliane-Joy , Jeandel Emmanuel , Zamdzhiev Vladimir 
Published: April 2023

AbstractVariational Quantum Algorithms are hybrid classical-quantum algorithms where classical and quantum computation work in tandem to solve computational problems. These algorithms create interesting challenges for the design of suitable programming languages. In this paper we introduce Qimaera, which is a set of libraries for the Idris 2 programming language that enable the programmer to implement hybrid classical-quantum algorithms where the full power of the elegant Idris language works in synchrony with quantum programming primitives. The two key ingredients of Idris that make this possible are (1) dependent types which allow us to implement unitary quantum operations; and (2) linearity which allows us to enforce fine-grained control over the execution of quantum operations so that we may detect and reject many physically inadmissible programs. We also show that Qimaera is suitable for variational quantum programming by providing implementations of two prominent variational quantum algorithms – QAOA and VQE.
Automatic Alignment in Higher-Order Probabilistic Programming Languages
Authors: Lundén Daniel , Çaylak Gizem , Ronquist Fredrik , Broman David 
Published: April 2023

AbstractProbabilistic Programming Languages (PPLs) allow users to encode statistical inference problems and automatically apply an inference algorithm to solve them. Popular inference algorithms for PPLs, such as sequential Monte Carlo (SMC) and Markov chain Monte Carlo (MCMC), are built around checkpoints—relevant events for the inference algorithm during the execution of a probabilistic program. Deciding the location of checkpoints is, in current PPLs, not done optimally. To solve this problem, we present a static analysis technique that automatically determines checkpoints in programs, relieving PPL users of this task. The analysis identifies a set of checkpoints that execute in the same order in every program run—they are aligned. We formalize alignment, prove the correctness of the analysis, and implement the analysis as part of the higher-order functional PPL Miking CorePPL. By utilizing the alignment analysis, we design two novel inference algorithm variants: aligned SMC and aligned lightweight MCMC. We show, through real-world experiments, that they significantly improve inference execution time and accuracy compared to standard PPL versions of SMC and MCMC.
Adversarial Reachability for Program-level Security Analysis
Authors: Ducousso Soline , Bardin Sébastien , Potet Marie-Laure 
Published: April 2023

AbstractMany program analysis tools and techniques have been developed to assess program vulnerability. Yet, they are based on the standard concept of reachability and represent an attacker able to craft smartlegitimateinput, while in practice attackers can be much more powerful, using for instance micro-architectural exploits or fault injection methods. We introduceadversarial reachability, a framework allowing to reason about suchadvanced attackersand check whether a system is vulnerable or immune to a particular attacker. As equipping the attacker with new capacities significantly increases the state space of the program under analysis, we present a new symbolic exploration algorithm, namelyadversarial symbolic execution, injecting faults in aforklessmanner to prevent path explosion, together with optimizations dedicated to reduce the number of injections to consider while keeping the same attacker power. Experiments on representative benchmarks from fault injection show that our method significantly reduces the number of adversarial paths to explore, allowing to scale up to 10 faults where prior work timeout for 3 faults. In addition, we analyze the well-tested WooKey bootloader, and demonstrate the ability of our analysis to find attacks and evaluate countermeasures in real-life security scenarios. We were especially able to find an attack not mentioned in a previous patch.
Automated Grading of Regular Expressions
Authors: Kim Su-Hyeon , Kim Youngwook , Han Yo-Sub , Im Hyeonseung , Ko Sang-Ki 
Published: April 2023

AbstractWith the rapid transition to distance learning, automatic grading software becomes more important to both teachers and students. We study the problem of automatically grading the regular expressions submitted by students in courses related to automata and formal language theory. In order to utilize the semantic information of the regular expression, we define a declarative logic that can be described by regular language and at the same time has natural language characteristics, and use it for the following tasks: 1) to assign partial grades for incorrect regular expressions and 2) to provide helpful feedback to students to make them understand the reason for the grades and a way to revise the incorrect regular expressions into correct ones. We categorize the cases when students’ incorrect submissions deserve partial grades and suggest how to assign appropriate grades for each of the cases. In order to optimize the runtime complexity of the algorithm, two heuristics based on automata theory are proposed and evaluated on the dataset collected from undergraduate students. In addition, we suggest Regex2NL which translates regular expressions to natural language descriptions to give insight to students so that they can understand how the regular expressions work.
Builtin Types Viewed as Inductive Families
Authors: Allais Guillaume 
Published: April 2023

AbstractState of the art optimisation passes for dependently typed languages can help erase the redundant information typical of invariant-rich data structures and programs. These automated processes do not dramatically change the structure of the data, even though more efficient representations could be available.Using Quantitative Type Theory as implemented in Idris 2, we demonstrate how to define an invariant-rich, typechecking-time data structure packing an efficient runtime representation together with runtime irrelevant invariants. The compiler can then aggressively erase all such invariants during compilation.Unlike other approaches, the complexity of the resulting representation is entirely predictable, we do not require both representations to have the same structure, and yet we are able to seamlessly program as if we were using the high-level structure.
Pragmatic Gradual Polymorphism with References
Authors: Ye Wenjia , Oliveira Bruno C. d. S. 
Published: April 2023

AbstractGradualizing System F has been widely discussed. A big challenge is to preserve relational parametricity and/or the gradual guarantee. Most past work has focused on the preservation of parametricity, but often without the gradual guarantee. A few recent works satisfy both properties by giving up System F syntax, or with some restrictions and the introduction of sophisticated mechanisms in the dynamic semantics.While parametricity is important for polymorphic languages, most mainstream languages typically do not satisfy it, for a variety of different reasons. In this paper, we explore the design space of polymorphic languages that satisfy the gradual guarantee, but do not preserve parametricity. When parametricity is not a goal, the design of polymorphic gradual languages can be considerably simplified. Moreover, it becomes easy to add features that are of practical importance, such as mutable references. We present a new gradually typed polymorphic calculus, called $$\lambda ^{G}_{gpr}$$

λ

gpr

G

, with mutable references and with an easy proof of the gradual guarantee. In addition, compared to other gradual polymorphism work, $$\lambda ^{G}_{gpr}$$

λ

gpr

G

is defined using a Type-Directed Operational Semantics (TDOS), which allows the dynamic semantics to be defined directly instead of elaborating to a target cast language. $$\lambda ^{G}_{gpr}$$

λ

gpr

G

and all the proofs in this paper are formalized in Coq.