Costruzioni modulari in linguaggi con tipi dipendenti.

In questa tesi si indaga come è possibile strutturare in modo modulare programmi e prove in linguaggi con tipi dipendenti. Il lavoro è sviluppato nel linguaggio di programmazione con tipi dipendenti Agda. Il fine è quello di tradurre l'approccio Datatypes à la carte, originariamente formulato per Haskell, in Type Theory: puntiamo ad ottenere un simile embedding di una nozione di sottotipaggio per tipi ricorsivi, che permetta sia la definizione di programmi con side-effect dove i diversi effetti sono definiti modularmente, che la modularizzazione di sintassi, semantica e ragionamento relativi a descrizioni di linguaggi.

Mathematical Modeling to Investigate Antiarrhythmic Drug Side Effects: Rate-Dependence Role in Ionic Currents and Action Potentials Shape in the O’Hara Model

Sudden cardiac death due to ventricular arrhythmia is one of the leading causes of mortality in the world. In the last decades, it has proven that anti-arrhythmic drugs, which prolong the refractory period by means of prolongation of the cardiac action potential duration (APD), play a good role in preventing of relevant human arrhythmias. However, it has long been observed that the “class III antiarrhythmic effect” diminish at faster heart rates and that this phenomenon represent a big weakness, since it is the precise situation when arrhythmias are most prone to occur. It is well known that mathematical modeling is a useful tool for investigating cardiac cell behavior. In the last 60 years, a multitude of cardiac models has been created; from the pioneering work of Hodgkin and Huxley (1952), who first described the ionic currents of the squid giant axon quantitatively, mathematical modeling has made great strides. The O’Hara model, that I employed in this research work, is one of the modern computational models of ventricular myocyte, a new generation began in 1991 with ventricular cell model by Noble et al. Successful of these models is that you can generate novel predictions, suggest experiments and provide a quantitative understanding of underlying mechanism. Obviously, the drawback is that they remain simple models, they don’t represent the real system. The overall goal of this research is to give an additional tool, through mathematical modeling, to understand the behavior of the main ionic currents involved during the action potential (AP), especially underlining the differences between slower and faster heart rates. In particular to evaluate the rate-dependence role on the action potential duration, to implement a new method for interpreting ionic currents behavior after a perturbation effect and to verify the validity of the work proposed by Antonio Zaza using an injected current as a perturbing effect.