Verificación de Sistemas Basada en Teoría de Tipos

Este proyecto se enmarca en la utlización de métodos formales (más precisamente, en la utilización de teoría de tipos) para garantizar la ausencia de errores en programas. Por un lado se plantea el diseño de nuevos algoritmos de chequeo de tipos. Para ello, se proponen nuevos algoritmos basados en la idea de normalización por evaluación que sean extensibles a otros sistemas de tipos. En el futuro próximo extenderemos resultados que hemos conseguido recientemente [16,17] para obtener: una simplificación de los trabajos realizados para sistemas sin regla eta (acá se estudiarán dos sistemas: a la Martin Löf y a la PTS), la formulación de estos chequeadores para sistemas con variables, generalizar la noción de categoría con familia utilizada para dar semántica a teoría de tipos, obtener una formulación categórica de la noción de normalización por evaluación y finalmente, aplicar estos algoritmos a sistemas con reescrituras. Para los primeros resultados esperados mencionados, nos proponemos como método adaptar las pruebas de [16,17] a los nuevos sistemas. La importancia radica en que permitirán tornar más automatizables (y por ello, más fácilmente utilizables) los asistentes de demostración basados en teoría de tipos. Por otro lado, se utilizará la teoría de tipos para certificar compiladores, intentando llevar adelante la propuesta nunca explorada de [22] de utilizar un enfoque abstracto basado en categorías funtoriales. El método consistirá en certificar el lenguaje "Peal" [29] y luego agregar sucesivamente funcionalidad hasta obtener Forsythe [23]. En este período esperamos poder agregar varias extensiones. La importancia de este proyecto radica en que sólo un compilador certificado garantiza que un programa fuente correcto se compile a un programa objeto correcto. Es por ello, crucial para todo proceso de verificación que se base en verificar código fuente. Finalmente, se abordará la formalización de sistemas con session types. Los mismos han demostrado tener fallas en sus formulaciones [30], por lo que parece conveniente su formalización. Durante la marcha de este proyecto, esperamos tener alguna formalización que dé lugar a un algoritmo de chequeo de tipos y a demostrar las propiedades usuales de los sistemas. La contribución es arrojar un poco de luz sobre estas formulaciones cuyos errores revelan que el tema no ha adquirido aún suficiente madurez o comprensión por parte de la comunidad.

HABLAR, LEER, ESCRIBIR COMO ACTIVIDADES FUNDANTES DE LOS APRENDIZAJES ESCOLARES"

A lo largo de cinco años, el Centro de Investigaciones Lingüísticas de la Facultad de Lenguas ha estudiado interdisciplinariamente lo relacionado a los aprendizajes y procesos de progreso lingüísticos en niños y adolescentes (Proyecto PICTOR 20293). La labor se desarrolló en equipo, conformado por especialistas del área Salud y del área Ciencias del Lenguaje (psico y sociolingüistas). Desde la salud, se indagó en lo relacionado a salud bucal, sistema estomatognático, nutrición y sus posibles incidencias en lo que a cognición y lenguaje se refiere. Desde las Ciencias del Lenguaje, fueron espacios específicos la conciencia fonológica, la disponibilidad léxica, la comprensión lectora, las cosmovisiones del docente, la escritura de textos, la construcción de los conocimientos. Gran parte de la tarea se desarrolló en las instalaciones de la Escuela Primaria Primer Teniente Ávila y allí se generó un fructífero intercambio de acciones y opiniones entre los investigadores y los docentes que fructificaron en pequeños programas de intervención en las aulas. Un perfil de un programa, esta vez de transferencia, estaba ya surgiendo en la comunidad constituida. La escuela actual batalla en muchos frentes. Se trata hoy de una institución requerida en tensión por el medio circundante lo que la sume en un continuo vaivén de obligaciones mayores y menores, pero, todas ellas perentorias e impostergables. En ese panorama es muy apreciada la posibilidad de contar con un apoyo en formación para todo el cuerpo docente en un área tan sensible como la lingüística. No existe aún en nuestro medio el diseño de una tarea coordinada en consecutividad y gradualidad para la educación lingüística. Se propone ahora un PROGRAMA DE TRABAJO PARA MEJORAR LA CALIDAD de la LECTURA Y de LA ESCRITURA (en particular en el segundo ciclo) y, consecuentemente, facilitar la permeabilidad de los aprendizajes escolares. La base de esos aprendizajes es lingüístico-cognitiva ya que lo que se enseña y se aprende se vehicula siempre bajo formato de lengua. En este sentido, hoy se insiste en "regresar al hablante" y tratar de develar qué sabe él de la lengua que habla, su “conciencia semántica" y, a partir de lo que se "des-cubra", se propondrá un punto de partida para iniciar el camino del desarrollo lingüístico-cognitivo. Uno de los inconvenientes en la actualidad es que no se establecen los hitos referenciales para la progresión, por etapa, de maduración del alumnado. Por ejemplo, se afirma que se enseña léxico porque los alumnos tienen "pobreza léxica", pero no circula ningún instrumento de apoyo que aleje la afirmación del mero impresionismo para conocer lo más técnicamente posible cuál es el léxico general disponible de cada grupo etario y, a partir de allí, proceder a las prácticas de incorporación de nuevas palabras. En este mismo sentido, la investigación desarrollada por el PICTOR se ocupó de lo referido a disponibilidad léxica (DL), prácticas y especulaciones fonológicas, morfológicas, conciencia textual y pragmática. Por esta razón la escuela descubrió instrumentales necesarios para contar con índices de DL, de madurez fonológico-morfológica según edad y áreas de conocimiento. Por todo lo dicho, la Escuela Primer Teniente Ávila requiere un programa de aplicación para mejorar la calidad de la lectura y de la escritura, en particular en el segundo ciclo (EGB2) con un diseño de objetivos específicos que, en su encadenamiento etapa a etapa, irá constituyendo una enseñanza-aprendizaje lingüístico-cognitiva programada para coadyuvar en la aprehensión de los conocimientos generales.