Como anuncié en un post anterior, se aproxima mi defensa de tesis: el 23 de Setiembre. A partir de Octubre comenzaré un postdoc en la Université de Paris-Nord (Paris XIII), un proyecto financiado por DIGITEO y la región Île-de-France. El responsable del proyecto de Michele Pagani, del Laboratoire d'Informatique de Paris Nord y el socio Gilles Dowek, director de uno de los 5 dominios de investigación del INRIA.
Título del proyecto:
ALAL: Algebraic approaches to lambda calculi
(Métodos algebraicos para cálculos lambda)
No voy a poner el proyecto entero acá, pero dejo el resumen corto (abajo la traducción al español)
The project focuses on formal foundations for language-based (especially static) techniques guaranteeing resource-related runtime properties of programs. The project belongs to the research area whose aim is to associate to a program a certification assuring some specific properties. We will derive the tools and techniques for our investigation from the field of logical proof-theory and semantics, with special interest in linear logic and λ-calculus. In particular, we will explore the new interactions between linear algebra and the formal methods approach to computation, recently arisen from the differential extension of linear logic and the algebraic λ-calculi. The expected result is a robust theoretical framework in which to develop static analysis and verification tools for non-deterministic paradigms, such as stochastic systems, concurrent computation, quantum programming, etc.
Y aquí una traducción:
El proyecto se centra en los fundamentos formales de las técnicas basadas en lenguaje (sobre todo estáticas) que garantizan propiedades de ejecución de los programas relacionadas con recursos. Este proyecto pertenece al área de investigación cuyo objetivo es asociar a un programa una certificación que garantice ciertas propiedades. Vamos a derivar las herramientas y técnicas de nuestra investigación del campo de la teoría de la demostración lógica y de la semántica, con especial interés en lógica lineal y cálculo lambda. En particular, vamos a explorar las nuevas interacciones entre álgebra lineal y enfoques de métodos formales recientemente surgidos a partir de la extensión diferencial de lógica lineal y de los cálculos lambda algebraicos. El resultado esperado es un framework sólido en el cual desarrollar herramientas de análisis estático y verificación para paradigmas no-determinísticos como sistemas estocásticos, computación concurrente, computación cuántica, etc.
0 comments:
Publicar un comentario