Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

Enfoques sobre la ciudadanía. Philosophical Perspectives on Citizenship.

La necesidad que da origen al presente proyecto se relaciona con la ausencia de un tratamiento de la cuestión de la ciudadanía que haga interactuar distintos enfoques filosóficos -el principal indicador de esta carencia es la ausencia de producciones académicas que den cuenta de la complejidad que adquiere la temática si se la aborda desde los problemas que nos proporcionan otras perspectivas filosóficas y políticas-. En este sentido, el problema general del proyecto apunta a hacer discutir diferentes abordajes conceptuales para pensar la ciudadanía. Específicamente, trabajamos a partir de dos enfoques: 1) la discusión entre liberales y comunitaristas y sus actuales derivas y 2) la cuestión de la biopolítica y su relación con la temática de la ciudadanía. Se procura revisar la discusión liberales-comunitaristas propia de las ciencias políticas, interpelándola a partir de conceptos como los de dominación, relaciones de poder, control sobre la vida, disciplina, entre otros provenientes de la filosofía práctica, la teoría social, las ciencias de la educación, etc. Nuestra investigación parte de la hipótesis de que hacer discutir las problemáticas que se disputan liberales-comunitaristas, con la Teoría Crítica de la Escuela de Frankfurt y con los recientes fenómenos biopolíticos, permite un abordaje que atiende a la efectiva complejidad de las prácticas de ciudadanía en nuestra vida en común en las sociedades democráticas contemporáneas. Esto permitirá complejizar los presupuestos con los que tradicionalmente se ha pensado la ciudadanía, a partir sobre todo de los fenómenos socio-políticos más recientes, como los nuevos movimientos sociales, las discusiones acerca de la legislación del aborto y la eutanasia, los esfuerzos de los estados nacionales por incrementar medidas de seguridad que van desde la imposición de fuertes barreras a la inmigración hasta la realización de guerras preventivas. Entendemos que estos, entre otros fenómenos, desafían la hermenéutica tradicional sobre la ciudadanía. Es de esta manera que se buscará comprender los límites y alcances de las ideas de ciudadanía, entendiéndola como un concepto histórico formador de subjetividades. La metodología se basa en una perspectiva interdisciplinaria que proporciona las herramientas para un análisis conceptual de la temática de la ciudadanía. Esta metodología está orientada al desarrollo de un marco teórico que resulte productivo para investigaciones de campo en las ciencias sociales, así como también para la elaboración de un material bibliográfico destinado a docentes abocados a la ciudadanía. Otro de los propósitos fundamentales es el de formar una red entre diferentes equipos de investigación a nivel nacional a partir de las “I Jornadas Nacionales sobre Ciudadanía” y de la organización de un seminario especializado con un profesor visitante. As far as the general topic of citizenship concerns philosophy, the theoretical problem of how to reconcile the different perspectives, assuming that this is an enterprise that can be done, remains an open question. Furthermore, the absence of academic material dealing with the problem seems to be a good indicator of this tendency. The main focus of the present Project aims at coping with some of the most notorious theoretical approaches to citizenship. More specifically, we will analyze the next two approaches: 1) the debate libertarians-communitarians and 2) the relationship between biopolitics and citizenship. Our purpose is to revise the discussion libertarians-communitarians incorporating concepts such as domination, power-relationships, life-control, among others that find their roots in practical philosophy, social theory, education and so on. To the extent that theories of citizenship are only provided with the usual conceptual machinery, some of the most remarkable phenomena of our democratic societies will stand for them out of reach: the existence of new social movements, abortion and euthanasia, inmigration, etc. Our hypothesis is that by making the debate libertarians-communitarians interact with the Critical Theory as well as with biopolitical concepts, we will be in a better position to try to understand these diverse phenomena. With the development of some sort of a new hermeneutics, we expect to criticize the old ideas related to citizenship and to re-elaborate them in a way that allows us to understand this concept in a less-fundamental, historical sense. Methodologically, we will adopt a multi-dimensional approach which expects to be fruitful to many other investigations in the area of social sciences. The Project pretends to be useful as a consultation resource for educators in a bibliographical index to design their curricula. At the same time,a seminar with a visiting profesor, the organization of a Congres will be our main objectives.