Verified compilation of C programs with a nominal memory model

Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfying the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt.

Categories of intuitive reasoning and GeoGebra 3D: an experience with Brazilian students

This work presents the result of the application of a didactic sequence designed to understand the concept of the Cavalieri’s Principle, supported by the GeoGebra application in its version for mobile phones - 3D Calculator. For this study, the Theory of Categories of Intuitive Reasoning, by Efraim Fischbein, was used as a conceptual basis. The objective of this work was to elaborate and develop a didactic sequence aiming to subsidize the learning of the Cavalieri’s Principle from GeoGebra, as a way to help the student in the construction of geometric reasoning, through visualization, perception and intuition. The methodology of this work is qualitative research, exploratory type, being carried out from a didactic sequence developed in two meetings remotely, due to the scenario of the COVID-19 pandemic. The target audience of this research is a group of students aged 15-17 years from a public school in Fortaleza - CE, Brazil. In summary, it is pointed out that the intuitive reasoning categories mobilized from the use of GeoGebra have great potential to stimulate the evolution of the student's geometric thinking, through the development of perception, intuition and geometric visualization.

Cognitive Biases: Mistakes or Missing Stakes?

Despite decades of research on heuristics and biases, evidence on the effect of large incentives on cognitive biases is scant. We test the effect of incentives on four widely documented biases: base-rate neglect, anchoring, failure of contingent thinking, and intuitive reasoning. In laboratory experiments with 1,236 college students in Nairobi, we implement three incentive levels: no incentives, standard lab payments, and very high incentives. We find that very high stakes increase response times by 40% but improve performance only very mildly or not at all. In none of the tasks do very high stakes come close to de-biasing participants.

A data efficient machine learning model for autonomous operational avalanche forecasting

Snow avalanches pose serious hazard to people and property in snow bound mountains. Snow mass sliding downslope can gain sufficient momentum to destroy buildings, uproot trees and kill people. Forecasting and in turn avoiding exposure to avalanches is a much practiced measure to mitigate hazard world over. However, sufficient snow stability data for accurate forecasting is generally difficult to collect. Hence forecasters infer snow stability largely through intuitive reasoning based upon their knowledge of local weather, terrain and sparsely available snowpack observations. Machine learning models may add more objectivity to this intuitive inference process. In this paper we propose a data efficient machine learning classifier using the technique of Random Forest. The model can be trained with significantly lesser training data compared to other avalanche forecasting models and it generates useful outputs to minimise and quantify uncertainty. Besides, the model generates intricate reasoning descriptions which are difficult to observe manually. Furthermore, the model data requirement can be met through automatic systems. The proposed model advances the field by being inexpensive and convenient for operational use due to its data efficiency and ability to describe its decisions besides the potential of lending autonomy to the process.

A Window into the Rational Mind: The Neural Underpinnings of Human Reasoning

Humans reason intuitively by relying on gut hunches or rationally through analytical contemplation. The majority of research on human reasoning has relied on behavioural data and thus the neural underpinnings of this process remain unclear. To address this, we had participants perform a classic reasoning task while electroencephalographic (EEG) data was recorded. Within our reasoning task, participants completed a series of base-rate word problems wherein their decisions were either biased by a provided stereotype or based on statistical probability. Post experiment, we defined participant rationality as the percentage of responses that were made based on likelihood. We then examined frontal theta neural oscillations and found that increased power in this frequency range was associated with increased rationality. Our findings imply that theta oscillations are sensitive to rationality and further that rational reasoning involves a diverse brain network relative to intuitive reasoning.

Digital Fuzzy Current Controlled Light-Emitting Diode Driver with Power Factor Correction

This paper presents the design and development of a fuzzy peak current controlled (FPCC) single-stage single-phase nonisolated AC/DC high-power factor LED drive. The proposed controller includes a fuzzy logic controller (FLC) in the loop voltage and a peak current controller in the loop current for an integrated nonisolated LED driver to attain a high-power factor (PF). The proposed control avoids complexities related to nonlinearities of the converter. The control action is initially derived from a group of rules written in accordance with experience and intuitive reasoning. The proposed technique is realized using a DSP processor (TI-TMS320F2812), which is capable of executing a high number of instructions in one cycle. A 70 W, 350 mA LED driver operating with an input of 90 V-230 V, 50 Hz was designed and implemented using MATLAB/Simulink. The results of the driver are in accordance with international regulations. The steady-state and transient responses are validated experimentally.

On The Contribution of Interest Expense (Income) on Total Output

A decrease in interest rate in traditional view of monetary policy transmission is linked to a lower cost of borrowing which eventually results into a greater spending in investment and a bigger GDP. However, a decrease in interest rate is also linked to a decrease in interest income which, in turn, affects the aggregate demand and total GDP. So far, no concerted effort has been made to investigate this positive inter-relation between interest income and GDP in the existing literature. Here in the first place we intuitively describe the inter-relation between interest income and output and then provide a micro-foundation of our intuitive reasoning in the context of a small endowment economy with finitely-lived identical households. Then we try to uncover the impact of nominal interest income on the macroeconomy using multiplier theory for a panel of some 04 (four) OECD countries. We define and calculate the corresponding multiplier values algebraically and then we empirically measure them using impulse response analysis under structural panel VAR framework. Large, consistent and positive values of the cumulative multipliers indicate a stable positive relationship between nominal interest income and output. Moreover, variance decomposition of GDP shows that a significant portion of the variance in GDP is attributed to interest income under VAR/VECM framework. Finally, we have shown how and where our analysis fits into the existing body of knowledge.

Beyond Moral Dilemmas: The Role of Reasoning in Five Categories of Utilitarian Judgment

Over the past two decades, the study of moral reasoning has been heavily influenced by Joshua Greene’s dual-process model of moral judgment, according to which deontological judgments are typically supported by intuitive, automatic processes while utilitarian judgments are typically supported by reflective, conscious processes. However, most of the evidence gathered in support of this model comes from the study of people’s judgments about sacrificial dilemmas, such as Trolley Problems. To which extent does this model generalize to other debates in which deontological and utilitarian judgments conflict, such as the existence of harmless moral violations, the difference between actions and omissions, the extent of our duty to help others, and the good justification for punishment? To find out, we conducted a series of five studies on the role of reflection in these kinds of moral conundrums. In Study 1, participants were asked to answer under cognitive load. In Study 2, participants had to answer under a strict time constraint. In Studies 3 to 5, we sought to promote reflection through exposure to counter-intuitive reasoning problems or direct instruction. Overall, our results offer strong support to the extension of Greene’s dual-process model to moral debates on the existence of harmless violations and partial support to its extension to moral debates on the extent of our duty to help others.