With the introduction of assisted driving, new challenges regarding visual attention have emerged, as drivers' primary task has shifted from driving to monitoring. Driver Monitoring Systems (DMS) have been developed as a countermeasure for visual distraction. The DMS triggers warnings, prompting drivers to redirect their attention to the road when it considers them as distracted. To date, research on DMS is limited, particularly regarding the impact of driving mode (manual vs. assisted) on its effectiveness. Furthermore, it remains unclear whether the DMS is effective, when no further instructions on the system are given. Therefore, a driving simulator study was conducted to examine both the impact of the driving mode and the system instruction, as well as their interplay on drivers' visual distraction. Participants (N = 125) drove either in manual or assisted mode, with the DMS being either inactive, active or active and instructed and glance metrics being measured in the initial and repeated trial. The proportion of long glances, number of glances and total glance duration served as dependent variables. Results show a significant effect of DMS, characterized by a reduced proportion of long glances and an increased number of glances, but only in assisted driving mode and when the DMS was instructed. There was no effect of the DMS in manual driving. Also, no effects of an active but uninstructed DMS regarding visual distraction were found. Therefore, the effectiveness of DMS is not inherently guaranteed but is contingent upon the driving mode and instruction.

In-vehicle voice assistants (VAs) can potentially enhance driving safety and user experience. However, their success depends on trust and acceptance. This study explores two influencing factors: (1) design-based and (2) performance-based attributes. In a driving simulator study, N = 53 participants engaged with VAs varying in anthropomorphic appearance and response latency. Results indicate that neither factor universally enhanced trust or acceptance. Instead, a nuanced interaction emerged: When response latency was short, anthropomorphic appearance had no impact. However, when response latency was long, both the non- and high-anthropomorphic VA were rated as more trustworthy than a low-anthropomorphic VA. Additionally, participants rated the high-anthropomorphic VA equally trustworthy across both latencies, suggesting a potential buffering effect of anthropomorphism under suboptimal performance conditions. Furthermore, trust fully mediated the relationship between the factors and acceptance, supporting models that conceptualize trust as a precursor of acceptance. Based on these insights, design recommendations were derived.

Inductive types are a fundamental abstraction mechanism in type theory and proof assistants, supporting the definition of data structures and rich specifications. Nested inductive types extend this mechanism by allowing constructors to use parametric types instantiated with the type being defined (lists or trees of the type to be defined). They are widely used in large verification projects – including CompCert, Iris, Verinum, and MetaRocq – to express complex, structured specifications. Despite this widespread use, the treatment of nested inductive types in both and is unsatisfactory. rejects many practical definitions while accepts definitions for which no usable elimination principle can be defined. Neither system provides reliable automatic generation of elimination principles. As a result, developers must define custom eliminators by hand, leading to fragility, duplication, and significant proof engineering overhead. This paper introduces a novel validity criterion for nested inductive types that guarantees that they can be elaborated into well-formed mutual inductive types. Under this criterion, the elimination principle for the original nested definition is provably equivalent to that of its elaborated mutual form. Our condition strictly generalizes Lean’s current check while ruling out exactly the problematic cases accepted in . Using this foundation, we give a systematic method for automatically generating correct elimination principles for nested inductive types, and we provide an implementation integrated into , along with an implementation plan for .

Dependently typed proof assistants offer powerful meta-programming features, which allow users to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running example: deriving instances for the Functor typeclass. This example is fairly simple, but realistic enough to highlight recurring difficulties with meta-programming: conceptual limitations of frameworks such as term representation – and in particular binder representation –, meta-language expressiveness, and verifiability, as well as current limitations such as API completeness, learning curve, and prover state management, which could in principle be remedied. We conclude with insights regarding features an ideal meta-programming framework should provide.

Driver monitoring systems (DMS) represent a camera-based countermeasure for visual distraction that detect distracted drivers in real-time and subsequently prompt them to look back on the road. However, the effectiveness of DMS in reducing distraction is still being debated, with studies yielding inconsistent results. A correct understanding of a technological system is a key determinant for its effectiveness in terms of enhancing safety. Therefore, addressing a previously unexplored factor in DMS research, this study investigated how drivers' explicit knowledge about DMS influences system effectiveness in reducing visual distraction. Previous studies showed that drivers' understanding of DMS is incomplete if drivers are not instructed. Therefore, in this study, the drivers' explicit knowledge of DMS was systematically manipulated between participants by providing verbal instructions prior to driving. Three experimental conditions were compared: drivers with explicit knowledge of DMS, drivers without knowledge, and a control group with an inactive DMS (between factor). Glance behavior was compared between the first and repeated interaction with the secondary task to assess visual distraction (within factor). Explicit knowledge significantly reduced the number of glances exceeding 2 s, indicating reduced visual distraction. This effect was prevalent, even after repeated interaction with the DMS. Importantly, mere activation of DMS without instruction did not affect glance behavior. Findings highlight the significant role of explicit knowledge in system effectiveness. The present work contributes to the field of DMS research by investigating drivers' mental model of DMS and deriving methodological and practical implications.

Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : ( Q -> A)-> R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardo, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant.

Touchscreens that offer various functions to the driver have become an integral part of the user interface in vehicles. To enable the use of these functions while preventing driver distraction, there is a trend towards implementing driver monitoring systems (DMS). DMS detect distraction and warn drivers accordingly. However, there is limited empirical evidence on the effectiveness of DMS in preventing visual distraction. Furthermore, potential interactions with contextual factors like secondary task complexity and task experience are neglected so far. Therefore, the present study investigated the effectiveness of a DMS, based on the Euro NCAP protocol, that issued warnings when long distraction (>= 3 s) or visual attention time sharing (>= 10 s in a 30 s window) occurred while driving on a highway. Glance behavior of 57 participants was analyzed while performing secondary tasks on an in-vehicle display with varying levels of task complexity and task experience. The effectiveness of the DMS depended on the task complexity and task experience. For more complex tasks, the DMS significantly reduced the number and total duration of glances to the display, but only for inexperienced trials. For experienced trials, no effect of the DMS was found. For less complex tasks, the DMS significantly reduced the duration of single glances and the proportion of long glances at the display, regardless of task experience. The results indicate that the effectiveness of DMS in reducing distraction is not as straightforward as assumed, emphasizing the importance of evaluating DMS in the context of contextual factors to draw accurate conclusions.

As in-vehicle voice assistants (IVVAs) become integral to modern driving experiences globally, it is essential to understand how their design impacts user experience (UX) across different cultures. Therefore, this study explores the interaction effects of visual appearance, system performance, and cultural background on both pragmatic and hedonic qualities of UX. In a driving simulator study, N = 105 participants from China and Germany interacted with IVVAs featuring varying levels of anthropomorphism (non-, low, high anthropomorphic) and response latency (short, long). The results revealed a universal preference for a short response latency. However, the impact of anthropomorphism on UX appears to be culturally dependent: While anthropomorphic design enhanced the hedonic qualities of UX for both Chinese and German participants, its impact on pragmatic UX qualities showed variation depending on cultural background. These findings underscore the necessity of adopting a user-centered, culturally-informed approach to IVVA design to optimize UX across diverse markets.

CoQ is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in CoQ is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in CoQ. This article presents the first implementation of a type checker for the kernel of CoQ (without the module system, template polymorphism and eta-conversion), which is proven sound and complete in CoQ with respect to its formal specification. Note that because of G & ouml;del's second incompleteness theorem, there is no hope to prove completely the soundness of the specification of CoQ inside CoQ (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the METACoQ project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of CoQ. It is worth mentioning that during the verification process, we have found a source of incompleteness in CoQ's official type checker, which has then been fixed in CoQ 8.14 thanks to our work. In addition to the kernel implementation, another essential feature of CoQ is the so-called extraction mechanism: the production of executable code in functional languages from CoQ definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for CoQ in the future.

In a driving simulator study, six experts interacted with an in-vehicle voice assistant (VA) and rated different latencies. The results suggest that in order to maintain drivers’ satisfaction with the interaction, in-vehicle VAs should have a latency of no more than 5 s. A slight delay of 1.5 s was rated best while shorter latencies caused highest variance amongst experts—indicating that the fastest response may not necessarily be the most desirable. Satisfaction may also depend on the complexity of the use case as experts showed higher tolerance toward longer latencies in the navigation-domain. Furthermore, our results raise thought-provoking insights about the importance of considering human expectations and preferences in the design of in-vehicle VAs. Despite technological advancements, humans might still expect a natural delay, similar to that in a human-human interaction. These findings emphasize the need to balance using cutting-edge technology with the desire for familiar interactions.

Driver Monitoring Systems (DMS) are designed to assist drivers by issuing warnings when distraction is detected. However, evidence from other warning systems suggests that warnings may also increase the workload of the driver. This study therefore examined the impact of DMS warnings on drivers’ workload, measured by the NASA TLX. Participants performed typical in-vehicle infotainment tasks during driving. For half of the tasks, the DMS was active and triggered warnings, whereas for the other half, it was inactive and did not trigger warnings. The results indicate that warnings, issued by the active DMS, resulted in a significantly higher self-reported workload, particularly in terms of higher perceived temporal demand and lower perceived performance. Furthermore, there was a significant positive correlation between the self-reported workload and the number of warnings. These findings underscore the necessity of carefully designing DMS to balance the benefits of distraction mitigation and the potential impacts on workload.

The Kleene-Post theorem and Post's theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees a la Kleene-Post and observe that the classical content of Post's theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.

Driver Monitoring Systems (DMS) detect visual distraction and alert drivers to maintain focus on the road. The European New Car Assessment Programme developed an algorithm that triggers warnings upon detecting distraction. Previous research showed that off-road glances during lane changes triggered warnings and drivers had difficulties understanding why these warnings occurred. Therefore, a simulator study was conducted in which drivers performed an overtaking maneuver in dense traffic. The DMS was either inactive and did not generate any warnings, or it was active and triggered warnings with or without being instructed beforehand. Results revealed that in 50 % of the overtaking maneuvers driving-related distraction was recorded. There was a significant difference between whether the DMS was inactive, active or instructed with regards to warnings. It was observed that side mirror glances, prior to overtaking, paradoxically prompted warnings. Findings indicated the necessity to refine DMS algorithms to discern safety-relevant behaviors from genuine distractions.

One of the central claims of fame of the Coq proof assistant is extraction, i.e. the ability to obtain efficient programs in industrial programming languages such as OCaml, Haskell, or Scheme from programs written in Coq’s expressive dependent type theory. Extraction is of great practical usefulness, used crucially e.g. in the CompCert project. However, for such executables obtained by extraction, the extraction process is part of the trusted code base (TCB), as are Coq’s kernel and the compiler used to compile the extracted code. The extraction process contains intricate semantic transformation of programs that rely on subtle operational features of both the source and target language. Its code has also evolved since the last theoretical exposition in the seminal PhD thesis of Pierre Letouzey. Furthermore, while the exact correctness statements for the execution of extracted code are described clearly in academic literature, the interoperability with unverified code has never been investigated formally, and yet is used in virtually every project relying on extraction. In this paper, we describe the development of a novel extraction pipeline from Coq to OCaml, implemented and verified in Coq itself, with a clear correctness theorem and guarantees for safe interoperability. We build our work on the MetaCoq project, which aims at decreasing the TCB of Coq’s kernel by re-implementing it in Coq itself and proving it correct w.r.t. a formal specification of Coq’s type theory in Coq. Since OCaml does not have a formal specification, we make use of the project specifying the semantics of the intermediate language of the OCaml compiler. Our work fills some gaps in the literature and highlights important differences between the operational semantics of Coq programs and their extraction. In particular, we focus on the guarantees that can be provided for interoperability with unverified code, and prove that extracted programs of first-order data type are correct and can safely interoperate, whereas for higher-order programs already simple interoperations can lead to incorrect behaviour and even outright segfaults.

The proposed test procedure presents an approach for the evaluation of the usability of partial automated driving HMI including driver monitoring systems in driving simulation. This procedure is based on a definition of requirements that a Level 2 HMI and its included driver monitoring system must fulfill in order to guarantee that the drivers understand their responsibilities of continuously monitoring the driving environment and the status of the partial automated driving system. These requirements are used to define the evaluation criteria that have to be validated in the test as well as the use cases in which these criteria can be assessed. The result is a detailed and comprehensive test guide including the specification of the test drives, the necessary instructions, the test environment and the recruiting criteria for the test sample. • Evaluation of usability aspects of level 2 automated driving HMI including driver monitoring systems • Based on the definition of requirements for L2 HMI • Test guide including the definition of use cases, evaluation criteria and testing conditions in driving simulation

Download This Paper Open PDF in Browser Add Paper to My Library Share: Permalink Using these links will ensure access to this page indefinitely Copy URL Copy DOI

The present study investigated the effects of a driver monitoring system that triggers attention warnings in case distraction is detected. Based on the EuroNCAP protocol, distraction could either be long glances away from the forward roadway (≥3s) or visual attention time sharing (>10 cumulative seconds within a 30 s time interval). In a series of manual driving simulator drives, 30 participants completed both driving related tasks (e.g., changing multiple lanes in dense traffic) and non-driving related tasks (e.g., infotainment operations). Results of warning frequencies revealed that visual attention time sharing warnings occurred more frequently than long distraction warnings. Moreover, there was a large number of attention warnings during driving related tasks. Results also revealed that participants' mental models tended to be less accurate when it came to understanding of the visual attention time sharing warnings as compared to the long distraction warnings, which were understood more accurately. Based on these observations, the work discusses the applicability and design of driver monitoring warnings.

The design of automotive human–machine interfaces (HMIs) for global consumers’ needs to cater to a broad spectrum of drivers. This paper comprises benchmark studies and explores how users from international markets—Germany, China, and the United States—engage with the same automotive HMI. In real driving scenarios, N = 301 participants (premium vehicle owners) completed several tasks using different interaction modalities. The multi-method approach included both self-report measures to assess preference and satisfaction through well-established questionnaires and observational measures, namely experimenter ratings, to capture interaction performance. We observed a trend towards lower preference ratings in the Chinese sample. Further, interaction performance differed across the user groups, with self-reported preference not consistently aligning with observed performance. This dissociation accentuates the importance of integrating both measures in user studies. By employing benchmark data, we provide insights into varied market-based perspectives on automotive HMIs. The findings highlight the necessity for a nuanced approach to HMI design that considers diverse user preferences and interaction patterns.