Dartmouth Institute for Health Policy and Clinical Practice
Dartmouth Digital Commons (Dartmouth College)Not a member yet
8214 research outputs found
Sort by
Viability and Generalizability of Canonical Oscillation-based Theories in the Rodent Ventral Striatum and Hippocampus
This thesis investigates the viability and generalizability of two prominent oscillation-based theories in the rodent limbic system: “communication through coherence” (CTC) in the ventral striatum (vStr) and “theta sequence” coding in the hippocampus. First, we tested fundamental physiological requirements for the CTC hypothesis, which posits that the vStr flexibly routes convergent inputs by modulating oscillatory coherence. We used simultaneous optogenetics and electrophysiology in awake, head-fixed mice to test the first requirement: phase-dependent excitability. We found that a third of vStr PV+ interneurons exhibit the hypothesized phase-dependent excitability, providing the first direct physiological evidence for this foundational component of CTC in the local circuitry. Next, we tested a second requirement for CTC : the existence of a flexible switching mechanism. We analyzed spiking and LFP data from rats, testing the in vitro-based hypothesis that Medium Spiny Neurons (MSNs) act as a switch by systematically changing their phase-locking frequency with their firing rate. Our results did not support this specific hypothesis. MSNs showed highly heterogeneous, non-systematic changes, refuting this proposed mechanism. We then moved to the hippocampus to test the generalizability of theta sequence coding to the non-spatial domain. We recorded dorsal CA1 neurons in head-fixed mice that were passively exposed to predictable and random odor sequences. Despite robust encoding of the current odor identity in both blocks, we found no evidence of the predicted Past-Current-Next theta sequence in the predictable block. Subsequent analyses using novelty and sequence-violation probes confirmed a lack of neural evidence for sequence learning. This thesis provides a mixed verdict on vStr CTC, confirming a key component while refuting a specific switching mechanism. Collectively, our findings suggest that these canonical oscillation-based theories are not a default processing mode, but are likely conditional mechanisms engaged only when the temporal structure of information becomes behaviorally relevant
AN ACTIVE ELECTRODE ELECTRICAL IMPEDANCE TOMOGRAPHY PROBE FOR INTRAOPERATIVE SURGICAL MARGIN ASSESSMENT IN ROBOTIC-ASSISTED RADICAL PROSTATECTOMIES
Prostate cancer is the most common cancer among men and the second most common cancer overall in the United States, with 288,300 new cases in 2023 and 1.4 million globally. Approximately 40.5% of patients undergo radical prostatectomy (RP), where the primary goal is complete tumor removal while preserving neurovascular structures and urethral length to maintain erectile function and continence. Achieving this balance contributes to variable positive surgical margin (PSM) rates, reported between 4–48% (average 21%). PSMs increase recurrence risk and often necessitate costly, noxious adjuvant therapies. Despite this there is no widely adopted method for intraoperative margin assessment in real time. Electrical impedance has shown promise in distinguishing malignant from benign prostate tissue in ex vivo studies. This dissertation presents the development, optimization, and evaluation of a broadband Electrical Impedance Tomography (EIT) system for intraoperative surgical margin assessment during robotic-assisted RP. A custom electrode array was optimized for tetrapolar measurements across 100 Hz–1 MHz. Integration with signal conditioning circuitry at the probe tip expanded bandwidth from 10 kHz–100 kHz in previous designs to 100 Hz–1 MHz with SNRs \u3e85 dB. In an ex vivo bovine model, complex 3D EIT reconstructions identified an optimal electrode pressure (2–5 kPa) and introduced a best fit factor (β) to improve permittivity reconstructions. Difference EIT at 100 Hz achieved sensitivity of 0.92, specificity of 0.90, and reconstruction time of 1.67 s, supporting real-time feasibility. Clinical studies collected 784 ex vivo and 154 in vivo impedance datasets across 64 patients, with fresh-section prostate data showing strong separation for malignancies \u3e50% of the sampled area. This work demonstrates a compact, laparoscopic compatible, high bandwidth active electrode EIT probe interfacing with the Da Vinci robotic system, enabling accurate and rapid image reconstructions, forming the foundation for real-time intraoperative margin assessment in RP
Using Design Thinking to Upcycle
This 60-minute lesson introduces the power of design thinking as a tool for sustainability. Through short discussions, visual examples, and a hands-on “Trash Island” design challenge, students will explore how creativity can transform waste into value. The session combines theory (understanding upcycling vs. recycling) with active practice (building prototypes from found materials). By the end, students will connect environmental responsibility to personal agency. They will realize that design can drive everyday impact
Machine Verification of Correctness for a Concurrent Union-Find Object
We consider a family of near-optimal randomized multiprocessor implementations for the union-find problem due to Jayanti and Tarjan–known as the Jayanti-Tarjan Randomized-Linking (JT-RL) union-find objects–and provide the first formal and fully machine-verified proof of their strong linearizability (i.e., correctness). Their algorithms are efficient both in theory and in practice: numerous benchmarking works demonstrate that they perform faster, or as fast, as all other known implementations for the union-find object on both CPUs and GPUs.
The correctness of the JT-RL algorithms is subtle, which motivates the need for formal verification. To this end, we first specify the JT-RL objects in TLA+, a formal specification language. We then provide a machine-verified proof of their strong linearizability, an extremely desirable property for concurrent algorithms which guarantees (among other things) that any algorithm A, deterministic or randomized, can use a JT-RL object in the place of an atomic union-find object without affecting the behaviors produced by A.
Our proof, written in TLA+ and verified using TLAPS, is intricate---spanning over 16,000 lines and organized into 20 theorems. Further, our modelling of the object, and of the corresponding proof, introduces many novel methods---including type isomorphisms, modelling randomness, and using nondeterminism to weaken specifications---which could aid future machine-verification efforts. Finally, because the proof is machine-certified, engineers can deploy these efficient union-find implementations with a robust guarantee of their correctness, enabling their widespread use without the need to reason explicitly over their possible behaviors
Safe Charging Locker for E-Bike Batteries
As the e-Bike market continues to grow without effective standardization, fatal battery fires (especially among cheaper alternative products) have become increasingly common. Dartmouth College (and many universities nationally) prohibit unsupervised indoor charging of e-Bikes without offering suitable alternative charging solutions. Enter the Fire-Safe e-Bike Charging Locker, which provides a safe charging location for e-Bike batteries. Targeting academic institutions and shared housing communities as buyers, the locker provides peace of mind and reduced insurance rates due to decreased safety risks. The locker prevents these fires through use of a thermal infrared camera, which detects abnormal increases in battery temperature before they reach dangerous levels, and initiates a battery shutoff. Currently, market solutions exist only to detect and extinguish fires, resulting in destruction of the battery. Our product allows for potential continued use of the battery, and a complete prevention of lithium-ion battery fires which can spread dangerously out of control
Pulse Electrothermal De-icing Air Source Heat Pumps for More Efficient Residential Renewable Energy Systems
Air source heat pumps (ASHPs) are increasingly being adopted as energy-efficient alternatives to traditional oil and gas furnaces for heating and cooling homes. However, in colder climates, these systems often face significant challenges due to frequent icing on the outdoor condenser fins during winter months. This icing condition drastically hinders performance by reducing efficiency, leading to higher energy consumption and increased operational costs. In the most common conventional defrosting method, the reversing valve sends refrigerant from the indoor space to the outdoor unit to melt the ice, effectively cooling the room. This defrosting process is both energy intensive and intermittently disruptive to heating functionality. To address this fundamental issue, the integration of the patented pulse electrothermal de-icing (PETD) technology into ASHP systems is explored. In this potential novel application, PETD technology efficiently removes ice and frost buildup through a series of high power pulses sent directly to the condenser fin system. This project analyzes the feasibility of advanced PETD and ASHP integration, with the potential for improved efficiency and lengthened operational lifespan for the ASHP unit, by reducing the mechanical stress caused by ice buildup. This advanced deicing solution demonstrates the potential for novel improvements to the reliability and performance of ASHPs, making them a more viable option for residential heating in regions with harsh winter conditions. The results ultimately highlight the need for further research into the potential of PETD and ASHP integration in overcoming environmental challenges and advancing efficient HV AC systems in our uncertain energy future
Modular HVAC Carbon Sequestration and Utilization Module
This project presents a modular post-combustion carbon capture system designed to integrate with existing HVAC infrastructure. Buildings contribute 39% of global energy-related carbon emis- sions, with 28% from operational sources including heating and cooling systems. Our solution addresses this significant emission source through retrofittable technology. The system employs 3M Liqui-Cel EXF membrane technology in air sweep mode, selected for cost-effectiveness, energy efficiency, and minimal spatial requirements. This design choice accom- modates remote locations and buildings with limited resources, as demonstrated in our Dartmouth Skiway case study. The membrane technology achieves 90% carbon capture efficiency with minimal modification to existing systems. Our analysis includes CO2 mass transfer modeling, economic assessment, and component specification. For commercial applications with multiple boilers, scaled implementations can substantially reduce a facility’s carbon footprint. Economic analysis shows carbon reduction costs of approximately 100 per ton of CO2 over 20 years when solar panels are used. The ultimate issue is that regardless of sequestration cost, the technology and process produces more net carbon than it sequesters over its operating lifetime, and so we must take steps to reduce CO2 produced in the first place. However, this technology represents a practical step toward meeting the World Green Building Council’s goal of net-zero operational carbon in all new buildings by 2030, while providing a solution for the substantial existing building stock that will continue operating for decades to come