Prácticas comunicativas forenses: Las relaciones intertextuales en el examen de testigos. Forensic communicative practices: intertextual relations in examination of witnesses.

Inscripto en el análisis del discurso interaccional de tradición angloamericana y optando por un abordaje metodológico etnográfico, este proyecto plantea investigar las relaciones entre textos orales y entre textos orales y escritos vinculados en cadenas textuales en un acontecimiento comunicativo institucional en el que tales relaciones tienen consecuencias directas en la confiabilidad de la información e intervienen en la construcción del conocimiento oficial. La situación comunicativa elegida es el examen y el contraexamen de testigos comunes durante procesos penales orales, de formato común no abreviado, en la jurisdicción de Córdoba capital. En las interacciones verbales con litigantes y jueces en las que emerge el testimonio se ponen en juego otros textos orales (en forma de citas de lo dicho antes por el mismo testigo u otras personas, referencias a rumores u opiniones colectivas, etc.) y textos escritos (actas de secuestro, informes periciales, actas de las declaraciones testimoniales en la etapa de instrucción, etc.). El foco de atención son las prácticas asociadas a la intertextualidad puesto que condicionan el carácter de la prueba testimonial producida ante el juzgador. Postulamos que los litigantes despliegan tácticas locales y estrategias globales reconocibles y recurrentes vinculadas al tratamiento de diversas categorías de textos previos. Además, planteamos averiguar si la participación de los jueces en interacción con los testigos es de suficiente injerencia como para ser un modo importante de generación de prueba testimonial. El enfoque metodológico general es etnográfico y analíticodiscursivo. Se seleccionará una causa por delito grave, se presenciará el debate en la cámara y se registrará el audio de todas las audiencias. Los datos a analizar serán los segmentos en las interacciones en los que se incorpora la lectura o se cita las actas de las declaraciones indagatorias o testimoniales anteriores, y los segmentos en los que se requiere, en calidad de prueba testimonial, la reproducción de dichos. Se procederá a partir de los detalles de la superficie textual y la pragmática de los intercambios y aprovechando el valor heurístico del concepto de voz, buscando identificar patrones recurrentes y los mecanismos generales que los rigen. Sobre esa base, se considerarán los intercambios verbales como interacción social que emerge moldeada por condiciones situacionales e institucionales y otros factores, tales como la incidencia de la pertenencia a grupos sociales o profesionales. Con el estudio se obtendrá una visión de prácticas cotidianas asociadas a la intertextualidad que son de crucial importancia para el carácter de la prueba testimonial producida ante el juzgador. Este paso nos acercará a conocer cómo se lleva a cabo efectivamente la administración de justicia penal y permitirá valorar los patrones de conducta a la luz de las normas procesales. In line with the Anglo-American tradition of situated discourse analysis, this project aims at tracing the links between oral texts and between oral and written texts related in textual chains which are present in an institutional event in which such relations have a direct consequence on the reliability of the information given and have an impact on the construction of what counts as official knowledge. The communicative situation under study is that of the direct and cross-examination of lay witnesses during a criminal trial in the city of Córdoba. During the face-to-face interactions between trial lawyers and judges in which the testimony takes place, other oral texts and written texts get incorporated. The focus of this research is centered on practices of intertextuality as they condition the nature of the oral evidence produced. It is argued that trial lawyers use recurrent local tactics and global strategies that are related to the treatment given to different categories of previous texts. Another aim of this study is to examine if judge’s interventions have an impact on the generation of the oral evidence. The data will come from a criminal trial that will be audio-taped in its entirety. Ethnographic observations of a criminal trial will be made. The focus of analysis will be on segments of interactions in which previous texts are read aloud or incorporated as quotes. After carrying out a detailed analysis of the surface of texts and the pragmatics of the exchanges, recurrent patterns and the general mechanisms that condition their emergence will be described. In this way, verbal exchanges will be considered social interactions that unfold conditioned by situational, institutional and social factors. This study will examine the relationship between intertextuality and the institutional practice of providing oral evidence. This will help understand how justice is actually administered and how patterns of behavior are valued according to institutional norms.

Verificación de Sistemas Basada en Teoría de Tipos. System verification in type theory

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. This project is about using type theory to garantee program correctness. It follows three different directions: 1) Finding new type-checking algorithms based on normalization by evaluation. First, we would show that recent results like [16,17] extend to other type systems like: Martin-Löf´s type theory without eta rule, PTSs, type systems with variables (in addition to systems in [16,17] which are a la de Bruijn), systems with rewrite rules. This will be done by adjusting the proofs in [16,17] so that they apply to such systems as well. We will also try to obtain a more general definition of categories with families and normalization by evaluation, formulated in categorical terms. We expect this may turn proof-assistants more automatic and useful. 2) Exploring the proposal in [22] to compiler construction for Algol-like languages using functorial categories. According to [22] such approach is suitable for verifying compiler correctness, claim which was never explored. First, the language Peal [29] will be certified in type theory and we will gradually add funtionality to it until a correct compiler for the language Forsythe [23] is obtained. 3) Formilizing systems for session types. Several proposals have shown to be faulty [30]. This means that a formalization of it may contribute to the general understanding of session types.