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.

Significance of GABAA Receptor for Cognitive Function and Hippocampal Pathology

The hippocampus is a primary area for contextual memory, known to process spatiotemporal information within a specific episode. Long-term strengthening of glutamatergic transmission is a mechanism of contextual learning in the dorsal cornu ammonis 1 (CA1) area of the hippocampus. CA1-specific immobilization or blockade of α-amino-3-hydroxyl-5-methyl-4-isoxazole-propionate (AMPA) receptor delivery can impair learning performance, indicating a causal relationship between learning and receptor delivery into the synapse. Moreover, contextual learning also strengthens GABAA (gamma-aminobutyric acid) receptor-mediated inhibitory synapses onto CA1 neurons. Recently we revealed that strengthening of GABAA receptor-mediated inhibitory synapses preceded excitatory synaptic plasticity after contextual learning, resulting in a reduced synaptic excitatory/inhibitory (E/I) input balance that returned to pretraining levels within 10 min. The faster plasticity at inhibitory synapses may allow encoding a contextual memory and prevent cognitive dysfunction in various hippocampal pathologies. In this review, we focus on the dynamic changes of GABAA receptor mediated-synaptic currents after contextual learning and the intracellular mechanism underlying rapid inhibitory synaptic plasticity. In addition, we discuss that several pathologies, such as Alzheimer’s disease, autism spectrum disorders and epilepsy are characterized by alterations in GABAA receptor trafficking, synaptic E/I imbalance and neuronal excitability.

Co-allocation to overlapping dendritic branches in the retrosplenial cortex integrates contextual memories across time

Events occurring close in time are often linked in memory, providing an episodic timeline and a framework for those memories. Recent studies suggest that memories acquired close in time are encoded by overlapping neuronal ensembles, and that this overlap is necessary for memory linking. Transient increases in neuronal excitability drive this ensemble overlap, but whether dendritic plasticity plays a role in linking memories is unknown. Here, we show that contextual memory linking is not only dependent on ensemble overlap in the retrosplenial cortex (RSC), but also on RSC branch-specific dendritic allocation mechanisms. Using longitudinal two-photon calcium imaging of RSC dendrites, we show that the same dendritic segments are preferentially activated by two linked (but not independent) contextual memories, and that spine clusters added after each of two linked (but not independent) contextual memories are allocated to the same dendritic segments. Importantly, with a novel optogenetic tool, selectively targeted to activated dendritic segments following learning, we show that reactivation of dendrites tagged during the first context exploration is sufficient to link two contextual memories. These results demonstrate a causal role for dendritic mechanisms in memory linking and reveal a novel set of rules that govern how linked, and independent memories are allocated to dendritic compartments.

A Locus Coeruleus- dorsal CA1 dopaminergic circuit modulates memory linking

Individual memories are often linked so that the recall of one triggers the recall of another. For example, contextual memories acquired close in time can be linked, and this is known to depend on temporary increase in excitability that drive the overlap between dorsal CA1 (dCA1) hippocampal ensembles encoding the linked memories. Here, we show that the Locus Coeruleus (LC) cells projecting to dCA1 have a key permissive role in contextual memory linking, without affecting contextual memory formation, and that this effect is mediated by dopamine and not by noradrenaline. Additionally, we found that LC to dCA1 projecting neurons modulate the excitability of dCA1 neurons, and the extent of overlap between dCA1 memory ensembles, as well as the stability of coactivity patterns within these ensembles. This discovery of a neuromodulatory system that specifically affects memory linking without affecting memory formation, reveals a fundamental separation between the brain mechanisms that modulate these two distinct processes.

CCR5 closes the temporal window for memory linking

Real world memories are formed in a particular context and are not acquired or recalled in isolation. Time is a key variable in the organization of memories, since events experienced close in time are more likely to be meaningfully associated, while those experienced with a longer interval are not. How does the brain segregate events that are temporally distinct? Here, we report that a delayed (12-24h) increase in the expression of the C-C chemokine receptor type 5 (CCR5), an immune receptor well known as a co-receptor for HIV infection, following the formation of a contextual memory, determines the duration of the temporal window for associating or linking that memory with subsequent memories. This delayed CCR5 expression in mouse dorsal CA1 (dCA1) neurons results in a decrease in neuronal excitability, which in turn negatively regulates neuronal memory allocation, thus reducing the overlap between dCA1 memory ensembles. Lowering this overlap affects the ability of one memory to trigger the recall of the other, thus closing the temporal window for memory linking. Remarkably, our findings also show that an age-related increase in CCL5/CCR5 expression leads to impairments in memory linking in aged mice, which could be reversed with a CCR5 knockout and an FDA approved drug that inhibits this receptor, a result with significant clinical implications. All together the findings reported here provide the first insights into the molecular and cellular mechanisms that shape the temporal window for memory linking.

Hippocampal-hypothalamic circuit controls context-dependent innate defensive responses

Preys use their memory - where they sensed a predatory threat and whether a safe shelter is nearby - to dynamically control their survival instinct to avoid harm and reach safety. However, it remains unknown which brain regions are involved, and how such top-down control of innate behaviour is implemented at the circuit level. Here, we show that the anterior hypothalamic nucleus (AHN) is best positioned to perform this task as an exclusive target of the hippocampus (HPC) within the medial hypothalamic defense system. Selective optogenetic stimulation and inhibition of hippocampal inputs to the AHN revealed that the HPC→AHN pathway not only mediates the contextual memory of predator threats but also controls the goal-directed escape by transmitting information about the surrounding environment. These results reveal a new mechanism for experience-dependent, top-down control of innate defensive behaviours.

The Role of the Nucleus Reuniens in Regulating Contextual Conditioning with the Predator Odor TMT

Experiencing intrusive distressing memories of a traumatic event(s) is a prominent symptom profile for post-traumatic stress disorder (PTSD). Understanding the neurobiological mechanisms associated with this symptom profile can be invaluable for effective treatment for PTSD. Here, we investigated the functional role of the nucleus reuniens (RE), a midline thalamic in modulating stressor-related memory. Female Long Evans rats were implanted with a cannula aimed at the RE. The RE was pharmacologically inactivated via muscimol (0.5 mM) prior to exposure to the predator odor stressor trimethylthiazoline (TMT; synthetically derived fox feces component) or water (controls) in a distinct context with bedding material (Experiment 1) or no bedding (Experiment 2). To measure context reactivity, the index of the contextual memory, 2 weeks following exposure to TMT, rats were re-exposed to the TMT-paired context (in the absence of TMT). In Experiment 1, during context re-exposure (with bedding), inactivation of the RE had no effect on context reactivity. In Experiment 2, during context re-exposure (no bedding), rats previous exposed to TMT showed decreased immobility compared to controls, indicating reactivity to the context and likely related to increased exploration of the environment. Rats in the TMT group that received RE inactivation showed increased immobility relative to rats that received aCSF, suggesting that muscimol pre-treatment blunted context reactivity. In conclusion, recruitment of the RE in stressor-related contextual memory appears to be dependent on the contextual environment and whether the animal is able to engage in different stress coping strategies.