Download Informe final de la estancia posdoctoral-joseraymundo

Document related concepts

Philip Wadler wikipedia , lookup

Transcript
Informe final de la estancia posdoctoral
1. Fecha del Informe: 15 de diciembre del 2009.
2. Nombre y Número del CVU del posdoctorante: José Raymundo Marcial Romero. CVU:
39478.
3. Programa de posgrado receptor: Maestría en Ciencias de la Computación.
4. Institución Receptora: Benemérita Universidad Autónoma de Puebla.
5. Título del proyecto de investigación: Semántica de lenguajes de programación para números
reales exactos.
6. Objetivos, metas y periodo propuesto para la estancia:
a. Objetivo: Extender el lenguaje de programación para números reales exactos llamado LRT
con tipos recursivos proponiendo un modelo matemático (semántica denotacional)
adecuado que permita demostrar cualquier propiedad que en la práctica tienen los
programas escritos en el lenguaje.
b. Metas:
i.
El planteamiento del objetivo antes mencionado se traducirá en: La presentación de
resultados parciales en alguno de los congresos nacionales e internacionales
relacionados con computación teórica o cómputo con números reales por ejemplo:
Sociedad Mexicana de Ciencias de la Computación (SMCC), Mathematical Foundation
of Programming Semantics (MFPS), Symposium of theoretical aspects in Computer
Science (STACS), Computability and Complexity in Analysis (CCA), Logic in Computer
Science (LICS), International Colloquium on Automata, Languages and Programming
(ICALP).
ii. La redacción de por lo menos un artículo para revistas internacionales con arbitraje que
incluirá los resultados planteados en el objetivo. Cabe mencionar que los resultados
implican la confirmación de las hipótesis planteadas. En caso de que alguna de las
hipótesis sea refutada, se buscará publicar el trabajo donde se explique el por que de
los resultados.
c. Periodo Propuesto para la estancia: Del 15 de Enero del 2009 al 14 de Enero del 2010.
7. Avances y descripción de los productos y/o metas comprometidos: Se presentó un
artículo en la conferencia internacional “Computability in Europe” en la cual se demostró la
convergencia de programas escritos en el lenguaje LRT. Los resultados fueron publicados en el
Abstract Booklet que se distribuyó durante el evento (se incluye como anexo). La conferencia
se llevó acabo en Heidelberg, Alemania. Se presentó un artículo en la conferencia Mexicana en
Computación denominada “Mexican International Conference in Computer Science” (ENC) que
organiza la Sociedad Mexicana de Ciencias. En este artículo se presenta la primer
implementación del lenguaje LRT y se compara con otras implementaciones existentes. La
conferencia se llevo acabo en el Distrito Federal. Los proceeding se publicarán por la IEEE
press. Se presentó un artículo en la conferencia “Logic and Non-monotonic Reasoning”. En
este artículo se demostró que todas las funciones de primer orden se pueden definir en el
lenguaje LRT. La conferencia se llevo acabo en Tlaxcala, México. Los proceedings del evento
se publicaron en CEUR Workshops proceedings (se incluye el artículo en anexo). Finalmente,
del último artículo publicado en CEUR, se invitó al autor a enviar una versión extendida del
mismo para que sea publicada en la Revista Inteligencia Artificial, la cual esta reconocida por
Latinindex, dbpl, redalyc y scopus. El artículo será enviado en Enero del 2010. Adicionalmente,
se tiene contemplado enviar una versión extendida del artículo presentado en el ENC a la
revista Computación y Sistemas indexada por el CONACYT.
8. Actividades desarrolladas en apoyo al fortalecimiento de la calidad del programa de
posgrado receptor vinculada al proyecto de investigación. Impartí dos cursos en la
Maestría en Ciencias de la computación, el primero en el verano del 2009 y el segundo en el
otoño del 2009. El primer curso denominado Tópicos Selectos en el cual elegí impartir
Semántica de Lenguajes de Programación, ya que es el fundamento de la investigación que
estoy realizando. El segundo curso denominado Lenguajes Formales y Autómatas, también
relacionado con la investigación que se desarrolló ya que se estudiaron las técnicas para
formalizar un lenguaje de programación. Impartí tres seminarios de Investigación. El primero
denominado “Topología Sintética de tipos de datos” en donde presenté como se puede utilizar
la topología para demostrar propiedades de programas en un lenguaje de programación. El
segundo seminario, denominado “Model Checking”, presenté cómo se pueden utilizar los
lenguajes formales para verificar propiedades de un programa en un lenguaje que contiene
concurrencia. Finalmente, una segunda parte del seminario “Model Checking” en el cual mostré
como se pueden utilizar herramientas computaciones para verificar propiedades de programas
de acuerdo a se especificación. De los resultados de los seminarios de “Model Checking”, se
envió a evaluación un artículo para conferencia en el cual participan dos estudiantes como
coautores. Pertenezco al comité tutorial del estudiante Angel Marín quien realiza sus estudios
en el programa de Maestría en Ciencias de la Computación de la BUAP.
9. Cronograma de las actividades generales desarrolladas
Periodo: de 01/2009 al 12/2009
Actividad
Fecha
de inicio
Escritura del artículo “An evolutionaryDiciembre
path planner for multiple robot arms”. 2009.
Fecha
Meta o Producto
de término
Enero
2009.
Artículo Publicado en abril del 2009 en
Lecture Notes in Computer Science,
número 5484.
Escritura del artículo “A Simulator forEnero 2009. Febrero
teaching
automata
and
formal
2009.
languages”.
Artículo Publicado en Mayo del 2009 en
Proceedings of the 11th International
Conference for Enterprise Information
Systems. La conferencia se llevó a cabo
en Milán, Italia.
Diseñar los constructores para extender Enero 2009. Febrero
el lenguaje con tipos de datos
2009.
recursivos, además de proponer la
Se establecieron las reglas operacionales
del lenguaje LRTp así como la forma en
semántica
mismos.
operacional
para
los
que funcionan los constructores.
Lectura de la tesis final de la alumna deEnero 2009. Febrero
licenciatura Rosaura García Firo en la
2009.
UAEM.
Obtención del título de la alumna Rosaura
García Firo.
Escritura
del
artículo
“AnAbril 2009.
implementation of exact real number
computation base on LRT”.
Abril
2009.
Artículo Publicado en Julio del 2009 en
“Abstract booklet of CIE”. La conferencia
se llevó a cabo en Heindelberg, Alemania.
Preparación e impartición del SeminarioFebrero
“Topología Sintética de tipos de datos y2009.
espacios clásicos”.
Abril
2009.
Elaboración de material didáctico para la
presentación del seminario.
Escritura del reporte final para elMarzo 2009. Marzo
proyecto 2438/2007 registrado ante la
2009.
UAEM.
Oficio de finiquito por parte de la UAEM
recibido el 19 de mayo del 2009.
Participación en la elaboración de
temarios para la Licenciatura
Computación de la Facultad
Ciencias de la Computación de
BUAP.
losEnero 2009. Nov.
en
2009.
de
la
Constancias de participación por parte del
Secretaria Académico de la Facultad de
Ciencias de la Computación de la BUAP.
Preparación e impartición del SeminarioMarzo 2009. Mayo
“Model Checking”.
2009.
Elaboración de material didáctico para la
presentación del seminario.
Escritura del artículo “ComparingMayo 2009. Mayo
implementations of a calculator for
2009.
exact real number computation”.
Artículo presentado en Sept. del 2009 en
la conferencia “Mexican International
conference on Computer Science”. La
conferencia se llevó a cabo en México
Distrito Federal.
Evaluación
PROMEP.
de
Nuevos
PTCs
enJunio 2009. Junio 2009. Constancia de participación expedida por
la Coordinadora Académica del PROMEP.
Preparación e impartición del SeminarioJunio 2009. Julio
“Model Checking y sus aplicaciones”.
2009.
Elaboración de material didáctico para la
presentación del Seminario. Envío de un
artículo a la conferencia CONIELECOMP
2010.
Presentación
del
artículo
“An19 de JulioJulio
implementation of exact real numberdel 2009.
2009.
computation base on LRT” en la
conferencia Computability in Europe.
Constancia de presentación del trabajo de
investigación ante pares académicos. La
constancia la expide el organizador del
congreso del CIE 2009.
Establecer la semántica denotacional01
MarzoAgo.
del lenguaje LRTp.
2009.
2009.
Resultados para su publicación en un
congreso nacional o internacional.
Escritura del artículo “Growing plants01 Ago.
for virtual 3D Environments”.
2009
Artículo publicado en los proceedings del
CCE 2009, el cual aparece en la IEEE
press. La conferencia se llevó a cabo en
Ago.
2009.
Toluca, Edo. de México.
Escritura del artículo “Functional First01 Ago.
Order Definability of LRTp”.
2009
Sept.
2009.
Artículo publicado en CEUR Proceeding
en la conferencia LANMR 2009. La
conferencia se llevó a cabo en Apizaco,
Tlaxcala.
Revisión de dos artículos para laSept. 2009. 01/10/09
conferencia LANMR 2009.
Constancia como revisor de dos artículos
sometidos para su publicación. La
constancia
la
expide
el
comité
organizador.
Presentación del artículo “ComparingSept. 2009. Sept.
implementations of a calculator for
2009.
exact real number computation”.
Artículo que será publicado por la IEEE
press en los Proceedings del ENC 2009.
Demostrar
la
adecuación1
computacional entre el lenguaje y la 2009.
semántica propuesta.
Lenguaje de programación para cómputo
con números reales exactos en donde se
puede definir cualquier función de primer
orden.
Sept.Dic.
2009.
Escritura de la versión extendida delSept. 2009. 01 Oct.
artículo “A Simulator for teaching
2009
automata and formal languages” que se
envió a la revista Transactions on
Computing Education (TOCE).
Correo electrónico de recepción por parte
del Comité evaluador de la ACM. Se
espera tener el artículo publicado en
revista para finales del 2010.
Preparación del artículo “A hybrid01 Oct.
algorithm for solving the rural postman 2009
problem”.
01 Oct.
2009
Artículo enviado para su evaluación por
pares académicos a la conferencia CCE
2009.
Preparación del artículo “Digital design01 Oct.
verification
based
on
P-stable 2009
semantics”.
01 Oct.
2009
Artículo enviado para su evaluación por
pares académicos a la conferencia
CONIELECOMP 2010.
Impartición de la Conferencia “Towards 10 de Nov.Nov.
a computacional Framework for exactde 2009.
2009.
real-number
computation”
en
la
conferencia CCE 2009.
Constancia de presentación por parte del
comité organizador del CCE. La
conferencia fue por invitación.
Evaluación de Cuerpos Académicos1Nov.
para la SEP.
2009
Nov.
2009.
Constancia de participación expedida por
la Coordinadora Académica del PROMEP.
Presentación
Presentación del
del artículo
artículo “Functional
“A hybrid5
7 de Nov. del
deNov.
Dic.
First
Order
Definability
of
LRTp”
en
el
2009.
2009.
algorithm for solving the rural postmandiciembre
2009.
congreso
LANMR
09.
problem” en el congreso CIC 2009.
del 2009.
Constancia
Constancia de
de presentación
presentación del
del trabajo
trabajo de
de
investigación
ante
pares
académicos.
investigación ante pares académicos. La
La
constancia la
la expide
expide el
el organizador
organizador del
del
constancia
congreso CIC
LANMR
2009.
congreso
2009.
Escritura de la versión extendida del1Nov.
artículo
“Functional
First
Order2009
Definability of LRTp” que se enviará a
evaluación a la Revista Inteligencia
Se espera tener el artículo publicado en la
revista Inteligencia Artificial a fnales del
2010.
Dic.
2009.
Artificial reconocida por LATININDEX.
Escritura de la versión extendida delDiciembre
artículo “Comparing implementations of2009.
a calculator for exact real number
computation” que se enviará a la revista
Computación y Sistemas reconocida
por CONACYT.
Enero
2010.
Se espera tener el artículo publicado en la
revista Computación Sistemas a finales
del 2010.
______________________________
__________________________________
Dr. José Raymundo Marcial Romero
Responsable del Proyecto
Dr. Ivo Humberto Pineda Torres
Secretario de Investigación y Estudios de Posgrado
Facultad de Ciencias de la Computación