• Datos Generales

    • Institución principal

      Universidad ORT Uruguay/ Universidad ORT Uruguay - Facultad de Ingeniería / Escuela de Ingeniería / Uruguay
    • Dirección institucional

      Institución: Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería / Sector Educación Superior/Privado
      / Escuela de Ingeniería
      Dirección: Cuareim 1451 / 11100 / Montevideo , Montevideo , Uruguay
      Teléfono: (598) 2902 1505 / 1378
      Correo electrónico/Sitio Web: tasistro@ort.edu.uy http://fi.ort.edu.uy/17586/5/version_en_espanol.html
  • Formación

    • Formación académica

      • Concluida

        • Doctorado

          • Computer Science (1990 - 1997)
            Universidad de Gotemburgo , Suecia
            Título de la disertación/tesis/defensa: Substitution, record types and subtyping in type theory, with applications to the theory of programming
            Tutor/es: Bengt Nordström
            Obtención del título: 1997
            Palabras Clave: Constructive Type Theory Theory of Programming
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación

          Maestría

          • Computer Science (1990 - 1993)
            Universidad de Gotemburgo , Suecia
            Título de la disertación/tesis/defensa: Formulation of Martin-Lof´s Theory of Types with Explicit Substitution
            Tutor/es: Bengt Nordström
            Obtención del título: 1993
            Financiación:
            Universidad Tecnológica de Chalmers , Suecia
            Palabras Clave: Constructive Type Theory Explicit Substitutions
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica de la Programación
        • Especialización/Perfeccionamiento

          • Diploma en Educación (2007 - 2008)
            Universidad ORT Uruguay - Universidad ORT Uruguay - Instituto de Educación , Uruguay
            Título de la disertación/tesis/defensa: Currículos Informáticos en Uruguay
            Tutor/es: Edith Litwin, Lila Pinto
            Obtención del título: 2008
            Financiación:
            Universidad ORT Uruguay / Facultad de Educación Internacional , Uruguay
            Palabras Clave: Educación Universitaria Diseño Curricular
            Areas de conocimiento:
            Ciencias Sociales / Ciencias de la Educación / Educación General / Educación Universitaria
        • Grado

          • Analista Programador (1980 - 1982)
            Universidad de la República - Facultad de Ingeniería - UDeLaR , Uruguay
            Título de la disertación/tesis/defensa:
            Obtención del título: 1982
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones /
  • Idiomas

    • Inglés
      Entiende muy bien / Habla muy bien / Lee muy bien / Escribe muy bien
    • Sueco
      Entiende bien / Habla bien / Lee muy bien /
    • Francés
      Entiende bien / Habla regular / Lee muy bien /
    • Portugués
      Entiende muy bien / Habla bien / Lee muy bien /
  • Areas de actuación

    • Ciencias Naturales y Exactas

      Ciencias de la Computación e Información /Ciencias de la Computación /Computación Teórica
    • Ingeniería y Tecnología

      Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información /Ingeniería de Sistemas y Comunicaciones /Métodos Formales en Ingeniería de Software
  • Actuación profesional

    • Sector Educación Superior/Privado - Universidad ORT Uruguay - Uruguay

      Universidad ORT Uruguay - Facultad de Ingeniería

      • Vínculos con la Institución

        • Funcionario/Empleado (02/2007 - a la fecha)Trabajo relevante
          Catedrático de Teoría de la Computación ,36 horas semanales / Dedicación total
        • Funcionario/Empleado (07/1997 - 02/2002)
          Docente ,10 horas semanales
      • Actividades

        • Líneas de investigación

          • Matemática y Programación en Teoría de Tipos (03/2009 - a la fecha )
            La Teoría Constructiva de Tipos es un sistema lógico que es a la vez una formalización de la Matemática (constructiva) y un lenguaje de programación funcional. Es particularmente relevante que esta teoría permita no sólo el desarrollo de (teoría de) programas, sino de una especie muy interesante de Matemática general. Se abre así la perspectiva no tan sólo de que los programas puedan ser tratados como objetos matemáticos, sino que, recíprocamente, los conceptos de la programación sean investigados como los conceptos matemáticos realmente relevantes. Dentro de esta línea, nos dedicamos al desarrollo de --técnicas de programación que hagan más efectiva la aplicación de la teoría, --metateoría de sistemas formales tales como lógicas y lenguajes de programación.
            Mixta
            8 horas semanales , Coordinador o Responsable
            Equipo: SZASZ, N , COPELLO, E.
            Palabras clave: Teoría de Tipos Matemática Constructiva Teoría de la Programación
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales de Ingeniería de Software
          • Didáctica de la Lógica, la Programación y la Matemática (03/2007 - a la fecha )
            Un problema fundamental del desarrollo de los métodos formales en Ingeniería de Software es el de la formación de recursos humanos, desde etapas tempranas, en las correspondientes teorías, métodos y tecnologías. Esto plantea problemas de didáctica, de la Programación, la Matemática, y la Lógica, que son de alto interés. Nos dedicamos al desarrollo de métodos y herramientas dirigidas a ayudar a prender a programar y demostrar.
            4 horas semanales , Coordinador o Responsable
            Equipo: MICHELINI, J.
            Palabras clave: didáctica de la programación didáctica de la Matemática
            Areas de conocimiento:
            Ciencias Sociales / Ciencias de la Educación / Educación General / Didáctica Universitaria
          • Estructuras de Sistemas Lógicos (03/2009 - a la fecha )
            Las estructuras de sistemas lógicos (logical frameworks) son lenguajes formales en los que es posible representar y razonar sobre sistemas formales en general. El objetivo en el plano tecnológico es disponer de plataformas de verificación formal de la infraestructura de los sistemas de programación, por ejemplo de compiladores y asistentes de demostración.
            Fundamental
            4 horas semanales , Coordinador o Responsable
            Equipo: SZASZ, N , FERNÁNDEZ, M.
            Palabras clave: logical frameworks
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
        • Proyectos de investigación y desarrollo

          • Desarrollo y Aplicaciones de la Teoría Constructiva de Tipos (12/2015 - a la fecha)
            Similar a la línea de investigación ya descripta. Se desarrolla en colaboración con un equipo de la Universidad Nacional de Córdoba, República Argentina.
            4 horas semanales
            Investigación
            Coordinador o Responsable
            En Marcha
            Alumnos encargados en el proyecto:
            Doctorado:1
            Financiación:
            Agencia Nacional de Investigación e Innovación, Uruguay, Apoyo financiero
            Equipo: SZASZ, N. , FRIDLENDER, D. , PAGANO, M.
            Palabras clave: Teoría de Tipos
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Design of a Type-Checking Algorithm for a Nominal Dependent Type System — Towards a Nominal Logical Framework (12/2015 - a la fecha)
            Se trata de implementar un sistema de razonamiento sobre sistemas formales tales como lógicas o lenguajes de programación basado en nuestros propios trabajos previos. La financiación es de la Embajada Británica.
            3 horas semanales
            Investigación
            Integrante del Equipo
            En Marcha
            Financiación:
            Embajada Británica en Uruguay, Gran Bretaña, Apoyo financiero
            Equipo: SZASZ, N (Responsable) , FERNÁNDEZ, M.
            Palabras clave: logical frameworks Nominal Abstract Syntax
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Métodos y Lenguajes de Programación en Teoría de Tipos (01/2013 - 01/2015 )
            -Desarrollo de métodos y tecnología para representar sistemas formales, e.g. lógicas y lenguajes de programación, y razonar sobre ellos. El objetivo en este caso es implementar en forma certificada los rasgos fundamentales de los múltiples lenguajes existentes. Estudiamos técnicas de razonamiento formal en Teoría Constructiva de Tipos sobre lenguajes con operadores de ligadura (nombres locales) ya sea a través del manejo de términos concretos usando substituciones múltiples, o de clases de equivalencia módulo renombre de nombres locales usando técnicas de la llamada sintaxis abstracta nominal. Asimismo, hemos realizado contribuciones en técnicas de programación en Teoría Constructiva de Tipos que permiten desarrollar programas con menor costo de código matemático explícito.
            5 horas semanales
            Investigación
            Integrante del Equipo
            Concluido
            Alumnos encargados en el proyecto:
            Doctorado:1
            Financiación:
            Agencia Nacional de Investigación e Innovación, Uruguay, Apoyo financiero
            Equipo: SZASZ, N
            Palabras clave: Teoría de Tipos Meta-teoría formalizada
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación /
          • Dependent Types for Nominal Terms (06/2009 - 10/2012 )
            Se desarrollan y estudian sistemas de tipos (dependientes) para la sintaxis nominal. Ésta es una alternativa a la notación tradicional empleada en Lógica en general y la Teoría de Tipos en particular para representar variables ligadas. El enfoque es promisorio desde el punto de vista teórico, principalmente en cuanto a la naturalidad de la teoría matemática de lenguajes que permite desarrollar. También constituye una alternativa interesante para el desarrollo de asistentes de demostración y otras herramientas computacionales asociadas a la teoría y tecnología de lenguajes de programación. Se realiza el proyecto en colaboración con una investigadora uruguaya del King´s College London y es financiada por la Royal Society británica.
            7 horas semanales
            Facultad de Ingeniería
            Investigación
            Integrante del Equipo
            En Marcha
            Financiación:
            Institución del exterior, Apoyo financiero
            Equipo: SZASZ, N (Responsable) , FERNÁNDEZ, M. (Responsable)
            Palabras clave: Sistemas de tipos Sintaxis Nominal
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica/ Teoría de Lenguajes de Programación
          • Types for Robust Program Development (03/2009 - 12/2011 )
            Se estudian cálculos de sistemas concurrentes, distribuidos y móviles que utilizan el concepto de tipo (de datos) para especificar comportamiento. Son de especial importancia los basados en el cálculo pi y sistemas de tipos tales como los "tipos de sesión". El desarrollo de la teoría correspondiente es delicado y hace conveniente su codificación en sistemas lógicos, utilizando herramientas de demostración semi-automática, con ell fin de garantizar su corrección. Se aspira a alcanzar una mejor comprensión de esta teorías también como consecuencia de su análisis formal. Este proyecto se realiza en colaboración con investigadores de Francia y Argentina y es financiada por el fondo francés de cooperación Stic-AmSud.
            7 horas semanales
            Facultad de Ingeniería
            Investigación
            Integrante del Equipo
            En Marcha
            Alumnos encargados en el proyecto:
            Maestría/Magister:1
            Financiación:
            Institución del exterior, Cooperación
            Equipo: SZASZ, N (Responsable) , BONELLI, E. (Responsable) , KESNER, D. (Responsable)
            Palabras clave: Teoría de Tipos Cálculos de concurrencia, distribución y movilidad
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica/ Teoría de Lenguajes de Programación
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales en Ingeniería de Software
          • Verificación de Transformaciones de Modelos de Comportamiento Basados en UML (03/2009 - 12/2011 )
            Se estudia y desarrolla la aplicación de métodos formales a la Ingeniería Dirigida por Modelos. Ésta es una orientación de la Ingeniería de Software que trata de elevar el nivel de abstracción de la producción efectiva de software al de los modelos estructurales y de comportamiento que habitualmente son el resultado de las actividades de Análisis y Diseño pero no de producción propiamente dicha. En este contexto, nuestro aporte reside en el desarrollo de experiencia. tecnología y teoría de la aplicación de sistemas lógicos como los descriptos arriba a los procesos de diseño de modelos y de transformaciones de modelos. El proyecto cuenta con financiación de Microsoft a través del fondo LACCIR y se realiza en colaboración con investigadores argentinos.
            7 horas semanales
            Facultad de Ingeniería
            Investigación
            En Marcha
            Alumnos encargados en el proyecto:
            Maestría/Magister:1
            Doctorado:1
            Financiación:
            Institución del exterior, Apoyo financiero
            Equipo: SZASZ, N (Responsable) , LUNA, C. , PONS, C. (Responsable)
            Palabras clave: Ingeniería Dirigida por Modelos Teoría de Tipos
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica/ Teoría de Lenguajes de Programación
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales en Ingeniería de Software
        • Docencia

          • Master en Ingeniería (03/2009 - a la fecha)
            Maestría
            Responsable
            Asignaturas:
            Lógica de la Programación, 4 horas, Teórico-Práctico
            Teoría de Tipos, 4 horas, Teórico-Práctico
            Algoritmos, Estructuras de Datos y Lenguajes Avanzados, 4 horas, Teórico-Práctico
          • Master en Ingeniería (03/2009 - a la fecha)
            Maestría
            Responsable
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Ingeniería en Sistemas (03/2015 - a la fecha)
            Grado
            Responsable
            Asignaturas:
            Teoría de la Computación, 4 horas, Teórico-Práctico
            Lenguajes de Programación, 5 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Ingeniería en Sistemas (08/2013 - 03/2015 )
            Grado
            Responsable
            Asignaturas:
            Fundamentos de la Computación, 5 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Ingeniería en Sistemas (03/2003 - 08/2013 )
            Grado
            Responsable
            Asignaturas:
            Lógica, 5 horas, Teórico
            Sistemas Formales de Computación, 4 horas, Teórico
            Segundo curso de Lógica para Ciencia de la Computación, 4 horas, Teórico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la computación
          • (03/2012 - 07/2012 )
            Maestría

            Asignaturas:
            Lógica de la Programación, 3 horas, Teórico-Práctico
            Teoría de Tipos, 3 horas, Teórico
          • Master en Ingeniería (08/2011 - 12/2011 )
            Maestría
            Responsable
            Asignaturas:
            Fundamentos de Lenguajes de Programación, 3 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Master en Ingeniería (03/2011 - 07/2011 )
            Maestría
            Responsable
            Asignaturas:
            Lógica de la Programación, 4 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • (08/2009 - 12/2009 )
            Maestría

            Asignaturas:
            Sistemas formales de computación distribuida, 4 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica/ Teoría de Lenguajes de Programación
          • (03/2009 - 07/2009 )
            Maestría
            Responsable
            Asignaturas:
            Teoría de Tipos, 4 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica/ Teoría de Lenguajes de Programación
          • Licenciatura en Análisis de Sistemas de Información (03/1997 - 12/2002 )
            Grado

            Asignaturas:
            Programación 1, 6 horas, Teórico-Práctico
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Programación
        • Gestión Académica

          • Dirección de la Cátedra de Teoría de la Computación (02/2002 - a la fecha )
            Facultad de Ingeniería
            Gestión de la Enseñanza
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la computación
          • Coordinador Académico del Máster en Ingeniería (02/2009 - a la fecha )
            Facultad de Ingeniería
            Gestión de la Enseñanza
          • Redacción del Plan de Estudios del Máster en Ingeniería (11/2007 - 12/2008 )
            Facultad de Ingeniería
            Gestión de la Enseñanza
    • Sector Educación Superior/Público - Programa de Desarrollo de las Ciencias Básicas - Uruguay

      Área Informática (PEDECIBA)

      • Vínculos con la Institución

        • Otro (03/1998 - a la fecha)Trabajo relevante
          Area Informática, Investigador Grado 3 ,1 hora semanal
          En Marzo de 2013 mi desempeño en el cargo fue evaluado por un tribunal internacional integrado por: - Dra. Irene Loiseau (Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires) - Dr. Claude Puech (Institut National de Recherche en Informatique et en Automatique - INRIA Chile) - Dr. Enrique Lessa (Facultad de Ciencias, UdelaR / PEDECIBA Biología) La recomendación de los evaluadores es la siguiente: Álvaro Tasistro. Se desempeña en la Universidad ORT. Su área de trabajo es la teoría y tecnología de sistemas lógicos. Su producción científica reciente es de buen nivel. Ha orientado una tesis de doctorado y estudiantes de maestría, y actualmente orienta un estudiante de doctorado. Se recomienda su renovación como Investigador Grado 3.
        • Colaborador (03/1991 - 02/1998)
          Investigador Asociado ,1 hora semanal
      • Actividades

        • Líneas de investigación

          • Matemática y Programación en Teoría de Tipos (03/2009 - a la fecha )
            Ver Líneas de Investigación en Universidad ORT Uruguay.
            Mixta
            10 horas semanales , Coordinador o Responsable
            Equipo: SZASZ, N , COPELLO, E.
            Palabras clave: Teoría de Tipos Teoría de la Programación
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales en Ingeniería de Software
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Estructuras de Sistemas Lógicos (03/2009 - a la fecha )
            Ver Líneas de Investigación en Universidad ORT Uruguay.
            Fundamental
            4 horas semanales , Coordinador o Responsable
            Equipo:
            Palabras clave: logical frameworks
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
    • Sector Educación Superior/Público - Universidad de la República - Uruguay

      Facultad de Ingeniería - UDeLaR

      • Vínculos con la Institución

        • Funcionario/Empleado (07/1997 - 02/2007)
          Profesor Agregado ,40 horas semanales
          Escalafón: Docente
          Grado: Grado 4
          Cargo: Efectivo
        • Profesor visitante (11/1994 - 03/1995)
          Profesor Agregado ,20 horas semanales
          Escalafón: Docente
          Grado: Grado 4
          Cargo: Interino
        • Funcionario/Empleado (03/1986 - 12/1988)
          Asistente ,30 horas semanales
          Escalafón: Docente
          Grado: Grado 2
          Cargo: Interino
        • Funcionario/Empleado (03/1983 - 03/1986)
          Ayudante ,30 horas semanales
          Escalafón: Docente
          Grado: Grado 1
          Cargo: Interino
      • Actividades

        • Proyectos de investigación y desarrollo

          • Subtipos y Objetos en Teorías y Herramientas de Programación Basadas en Teoría de Tipos (02/1999 - 02/2002 )

            10 horas semanales
            Facultad de Ingeniería , Instituto de Computación
            Investigación
            Coordinador o Responsable
            Concluido
            Alumnos encargados en el proyecto:
            Pregrado:3
            Equipo: BETARTE, G
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
          • Estructuras para Sistemas Lógicos (08/1994 - 08/1997 )

            5 horas semanales
            Facultad de Ingeniería , Instituto de Computación
            Desarrollo
            Integrante del Equipo
            Concluido
            Alumnos encargados en el proyecto:
            Pregrado:8
            Maestría/Magister:2
            Doctorado:3
            Equipo: BETARTE, G , CABEZAS, J (Responsable) , CALDERÓN, G. , DA ROSA, S. , SZASZ, N , GIMENEZ, E.
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
        • Docencia

          • Maestría en Informática (UDELAR-PEDECIBA) (07/1997 - 02/2007 )
            Maestría

            Asignaturas:
            Computabilidad y Complejidad, 6 horas, Teórico
            Lógica de la Programación Imperativa, 6 horas, Teórico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la computación
          • Ingeniería en Computación (07/1997 - 02/2007 )
            Grado

            Asignaturas:
            Lógica, 5 horas, Teórico
            Teoría de la Computación, 6 horas, Teórico
            Lógica de la Programación Imperativa, 6 horas, Teórico
            Programación 2, 6 horas, Teórico-Práctico
            Dirección de trabajos de Graduación, 5 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la computación
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Programación
          • Maestría en Informática (UDELAR-PEDECIBA) (11/1994 - 03/1995 )
            Maestría

            Asignaturas:
            Cálculo Lambda, 6 horas, Teórico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la computación
          • Maestría en Informática (UDELAR-PEDECIBA) (11/1990 - 12/1990 )
            Maestría

            Asignaturas:
            Revisión de Fundamentos de la Matemática, 6 horas, Teórico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
          • Ingeniería en Computación (03/1983 - 12/1986 )
            Grado

            Asignaturas:
            Programación I, 6 horas, Teórico-Práctico
            Programación III, 6 horas, Teórico-Práctico
            Procesamiento de datos I, 6 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Programación
        • Servicio Técnico Especializado

          • (03/1999 - 12/2001 )
            Facultad de Ingeniería, Instituto de Computación
            10 horas semanales
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones /
          • (03/1998 - 12/1998 )
            Facultad de Ingeniería, Instituto de Computación
            10 horas semanales
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones /
        • Gestión Académica

          • Coordinador responsable del área de Programación (07/1997 - 02/2007 )
            Facultad de Ingeniería, Instituto de Computación
            Gestión de la Enseñanza
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Programación
          • Redacción del programa de estudios y plan de puesta en marcha de la carrera de Tecnólogo Informático (UdelaR – UTU) (03/2005 - 12/2006 )
            Facultad de Ingeniería, Instituto de Computación
            Gestión de la Enseñanza
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones /
          • Delegado Docente en la Comisión de Instituto (03/2002 - 12/2004 )
            Facultad de Ingeniería, Instituto de Computación
            Participación en consejos y comisiones
    • Sector Extranjero/Internacional/Otros - Suecia

      Universidad de Gotemburgo

      • Vínculos con la Institución

        • Funcionario/Empleado (01/1990 - 07/1997)
          Candidato a Doctor ,40 horas semanales / Dedicación total
      • Actividades

        • Docencia

          • Bachelor of Science in Engineering (01/1990 - 07/1997 )
            Grado
            Responsable
            Asignaturas:
            Program Specification and Derivation, 6 horas, Teórico
            Programming, 6 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la computación
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Programación
    • Sector Extranjero/Internacional/Otros - Argentina

      Escuela Superior Latinoamericana de Informática

      • Vínculos con la Institución

        • Funcionario/Empleado (03/1987 - 12/1989)
          Instructor (Profesor Adjunto) ,40 horas semanales / Dedicación total
      • Actividades

        • Docencia

          • Licenciatura en Informática (03/1987 - 12/1989 )
            Grado
            Responsable
            Asignaturas:
            Algoritmos y Estructuras de Datos, 6 horas, Teórico-Práctico
            Lenguajes y Programación, 6 horas, Teórico
            Talleres de Programación, 6 horas, Teórico-Práctico
            Dirección de trabajos de Graduación y Pasantías Académicas, 5 horas, Teórico-Práctico
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Programación
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Paradigmas de Programación
  • Carga horaria

    • Carga horaria de docencia: 10 horas
    • Carga horaria de investigación: 14 horas
    • Carga horaria de formación RRHH: 14 horas
    • Carga horaria de extensión: Sin horas
    • Carga horaria de gestión: 6 horas
  • Producción científica/tecnológica

    • Me dedico a los fundamentos matemáticos de la Ingeniería de Software, es decir aquellas teorías que permiten razonar sobre los artefactos que se diseñan en el transcurso de la producción de programas, con el fin de evitar que las técnicas de validación queden reducidas al tratamiento de piezas de software como “cajas negras”. En el plano tecnológico, el objetivo es desarrollar lenguajes y sistemas de programación con la propiedad “si compila, funciona”, conocidos como compiladores "verificadores" o "certificadores".
      Es consecuencia de un teorema clásico de la Lógica que todo sistema que verifique automáticamente la corrección de código ejecutable respecto de especificaciones dadas debe necesariamente requerir del programador la producción de cierta evidencia de tal hecho. En otras palabras, el programador debe producir no sólo código ejecutable, sino también “código matemático” verificable por máquina. Los compiladores verificadores deben, por tanto, ser asistentes de demostración en los que resulte posible realizar cierta Matemática formalizada. El estado del arte de esta tecnología presenta múltiples herramientas, algunas de ellas de uso industrial.

      Los problemas relevantes del área son:

      -El desarrollo de teorías, lenguajes, y correspondientes sistemas de desarrollo, que modelen apropiadamente sistemas de software más realistas y versátiles, típicamente sistemas distribuidos.

      -El desarrollo de técnicas de programación ajustadas a las características de estos lenguajes y sistemas, que permitan reducir costos asociados a la producción de “código matemático”.

      Mis líneas de investigación dentro de este espacio son:

      -La Teoría Constructiva de Tipos, un sistema lógico que es a la vez una formalización de la Matemática (constructiva) y un lenguaje de programación funcional. Es particularmente relevante que esta teoría permita no sólo el desarrollo de (teoría de) programas, sino de una especie muy interesante de Matemática general. Se abre así otra perspectiva, i.e. no tan sólo de que los programas puedan ser tratados como objetos matemáticos, sino que, recíprocamente, los conceptos de la programación sean investigados como los conceptos matemáticos realmente relevantes.


      -Desarrollo de métodos y tecnología para representar sistemas formales, e.g. lógicas y lenguajes de programación, y razonar sobre ellos. El objetivo en este caso es implementar en forma certificada los rasgos fundamentales de los múltiples lenguajes existentes.

      Mis contribuciones recientes consisten en técnicas de razonamiento formal en Teoría Constructiva de Tipos sobre lenguajes con operadores de ligadura (nombres locales) ya sea a través del manejo de términos concretos usando substituciones múltiples, o de clases de equivalencia módulo renombre de nombres locales usando técnicas de la llamada sintaxis abstracta nominal. También hemos utilizado esta última teoría en el desarrollo de estructuras que permitan representar sistemas formales de manera directa y confiable. Asimismo, hemos realizado contribuciones en técnicas de programación en Teoría Constructiva de Tipos que permiten desarrollar programas con menor costo de código matemático explícito.
      Por último, un problema fundamental del desarrollo de los métodos formales en Ingeniería de Software es el de la formación de recursos humanos, desde etapas tempranas, en las correspondientes teorías, métodos y tecnologías. Esto plantea problemas de didáctica, de la Programación, la Matemática, y la Lógica, que son de alto interés.

  • Producción bibliográfica

    • Artículos publicados

      • Arbitrados

        • Machine-checked proof of the Church-Rosser theorem for the Lambda-Calculus using the Barendregt Variable Convention in Constructive Type Theory (Completo, 2018)Trabajo relevante
          TASISTRO, A. , Ernesto COPELLO , Nora SZASZ
          ENTCS, v.: 338 p.:79 - 95, 2018
          Palabras clave: Metateoría formal Cálculo Lambda Teoría Constructiva de Tipos
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          Medio de divulgación: Internet
          ISSN: 15710661
          DOI: 10.1016/j.entcs.2018.10.006
          https://www.sciencedirect.com/science/article/pii/S1571066118300720?via%3Dihub

        • Formal Metatheory of the Lambda Calculus Using Stoughton's Substitution (Completo, 2017)Trabajo relevante
          COPELLO, E. , SZASZ, N , TASISTRO, A.
          Theoretical Computer Science, v.: 685 p.:65 - 82, 2017
          Palabras clave: Lambda calculus Formal Metatheory Interactive Theorem Proving
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          Medio de divulgación: Papel
          Escrito por invitación
          ISSN: 03043975
          DOI: 10.1016/j.tcs.2016.08.025
          http://www.sciencedirect.com/science/article/pii/S0304397516304820

        • Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory (Completo, 2016)Trabajo relevante
          COPELLO, E. , TASISTRO, A. , SZASZ, N , BOVE A. , FERNÁNDEZ, M.
          ENTCS, v.: 323 p.:109 - 124, 2016
          Palabras clave: Type Theory Lambda calculus Formal Metatheory
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          Medio de divulgación: Internet
          ISSN: 15710661
          DOI: 10.1016/j.entcs.2016.06.008
          http://www.sciencedirect.com/science/article/pii/S1571066116300354

        • Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus (Completo, 2015)
          TASISTRO, A. , COPELLO, E. , SZASZ, N
          ENTCS, v.: 312 p.:215 - 230, 2015
          Palabras clave: Constructive Type Theory Fomalised Meta-theory
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          Medio de divulgación: Internet
          Escrito por invitación
          ISSN: 15710661
          DOI: 10.1016/j.entcs.2015.04.013

        • Proof Assistant Based on Didactic Considerations (Completo, 2013)Trabajo relevante
          PAIS, J. , TASISTRO, A.
          Journal of Universal Computer Science, v.: 19 11 , p.:1570 - 1596, 2013
          Palabras clave: educational software teaching logic software engineering education
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
          Ciencias Sociales / Ciencias de la Educación / Educación General / Software educativo
          Medio de divulgación: Internet
          Escrito por invitación
          ISSN: 09486968
          http://www.jucs.org/jucs_19_11/proof_assistant_based_on

        • PSPVDC: Una Propuesta que Incorpora el Diseño por Contrato Verificado al Personal Software Process. (Completo, 2013)
          MORENO, S. , TASISTRO, A. , VALLESPIR, D.
          Revista Latinoamericana de Ingeniería de Software, v.: 1 5 , p.:153 - 166, 2013
          Palabras clave: Métodos Formales Personal Software Process diseño por contrato
          Areas de conocimiento:
          Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
          Medio de divulgación: Internet
          ISSN: 23142642
          http://www.unla.edu.ar/sistemas/redisla/ReLAIS/ReLAIS-ediciones.htm

        • Principal Type Scheme for Session Types (Completo, 2012)
          TASISTRO, A. , COPELLO, E. , SZASZ, N
          International Journal of Logic and Computation, v.: 3 1 , p.:34 - 43, 2012
          Palabras clave: session types principal type schemes type inference algorithms
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          Medio de divulgación: Internet
          ISSN: 21801290
          http://www.cscjournals.org/csc/journals/IJLP/browsemanuscript.php?EJCode=72.73.75.79.99&JCode=IJLP&V

  • Libros

    • Twenty-five Years of Constructive Type Theory ( Participación , 1998)Trabajo relevante
      TASISTRO, A. , BETARTE, G
      Número de volúmenes: 1
      Edición: ,
      Editorial: Oxford Science Publications,
      Tipo de puplicación: Investigación
      Referado
      En prensa
      Palabras clave: Constructive Type Theory
      Medio de divulgación: Papel
      ISSN/ISBN: 0198501277
      Financiación/Cooperación:
      Gothenburg University / Beca, Suecia

      Capítulos:
      Extension of Martin-Löf`s type theory with record types and subtyping
      Organizadores:
      Página inicial 21, Página final 40
    • Programación Lógica y Funcional ( Libro publicado Texto integral , 1988)
      TASISTRO, A. , VIDART, J.
      Número de volúmenes: 1
      Número de páginas: 200
      Edición: ,
      Editorial: EBAI, Curitiba, Brasil
      Tipo de puplicación: Material didáctico
      Escrito por invitación
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Paradigmas de Programación
      Medio de divulgación: Papel
      ISSN/ISBN:
  • Documentos de Trabajo

    • PSP-VDC: An Adaptation of the PSP that Incorporates Verified Design by Contract (2013)
      Completo
      MORENO, S. , TASISTRO, A. , VALLESPIR, D. , NICHOLS, W.
      Serie: CMU-2013,
      Pittsburgh PA, USA
      Palabras clave: Measurement and Analysis Process Improvement
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
      Medio de divulgación: Internet
      http://resources.sei.cmu.edu/library/asset-view.cfm?assetID=47974
    • Fundamentos de la Computación (2013)
      Completo
      TASISTRO, A.
      Serie: 1, v: 1
      Universidad ORT Uruguay
      Palabras clave: Programación Funcional Matemática y Programación
      Areas de conocimiento:
      Ciencias Sociales / Ciencias de la Educación / Educación General / Currículos universitarios
      Medio de divulgación: Internet
      aulas.ort.edu.uy
    • Nominal Dependent Types as a Logical Framework (2011)
      Completo
      FEARWEATHER, E. , FERNÁNDEZ, M. , SZASZ, N , TASISTRO, A.
      Serie: 1, v: 11
      Kingś College London
      Palabras clave: nominal syntax dependent types logical frameworks
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Internet
      http://www.dcs.kcl.ac.uk/staff/maribel/
    • Experiment with a Type-Theoretic Approach to the Verification of Model Transformations (2009)
      Completo
      TASISTRO, A. , SZASZ, N , LUNA, C. , CALEGARI, D.

      Palabras clave: Ingeniería Dirigida por Modelos Teoría de Tipos Verificación Formal
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales en Ingeniería de Software
      Medio de divulgación: Papel
      http://www.ort.edu.uy/fi/pdf/documento8fi.pdf
    • Currículos Informáticos en Uruguay (2008)
      Completo
      TASISTRO, A.
      Serie: 115861, v: 1
      Palabras clave: Diseño Curricular Didáctica universitaria
      Areas de conocimiento:
      Ciencias Sociales / Ciencias de la Educación / Educación General / Didáctica Universitaria
      Medio de divulgación: Papel
    • Inducción y Recursión (2007)
      Completo
      TASISTRO, A.
      v: 1
      Universidad ORT Uruguay
      Palabras clave: Inducción y recursión
      Areas de conocimiento:
      Ciencias Sociales / Ciencias de la Educación / Educación General / Currículos universitarios
      Medio de divulgación: Internet
      aulas.ort.edu.uy
  • Publicación de trabajos presentados en eventos

    • Teaching of formal methods: evidence of its inclusion in curricula, results, and difficulties (2019)
      Completo
      MORENO, S. , VALLESPIR, D. , TASISTRO, A.

      Evento: Internacional
      Descripción: XXII Conferencia Iberoamericana de Software Engineering (CIbSE 2019)
      Ciudad: La Habana, Cuba
      Año del evento: 2019
      Publicación arbitrada
    • Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders (2018)
      Completo
      TASISTRO, A. , Ernesto Copello , Nora Szasz

      Evento: Internacional
      Descripción: Logical Frameworks and Meta-Languages; Theory and Practice (LFMTP 2018)
      Ciudad: Oxford, UK
      Año del evento: 2018
      Anales/Proceedings: Electronic Proceedings in Theoretical Computer Science
      Volumen:274
      Pagina inicial: 11
      Pagina final: 26
      ISSN/ISBN: 2075-2180
      Publicación arbitrada
      Palabras clave: Interactive Theorem Proving Formal Meta-Theory Lambda Calculus
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Internet
      DOI: 10.4204/EPTCS.274
      http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2018.2
    • Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution (2018)
      Completo
      TASISTRO, A. , COPES, M. , SZASZ, N

      Evento: Internacional
      Descripción: Logical Frameworks and Meta-Languages; Theory and Practice (LFMTP 2018)
      Ciudad: Oxford, UK
      Año del evento: 2018
      Anales/Proceedings: Electronic Proceedings in Theoretical Computer Science
      Volumen:274
      Pagina inicial: 27
      Pagina final: 41
      ISSN/ISBN: 2075-2180
      Publicación arbitrada
      Palabras clave: Interactive Theorem Proving Formal Meta-theory Lambda Calculus
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Internet
      DOI: 10.4204/EPTCS.274
      http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2018.3
    • Machine-checked proof of the Church-Rosser theorem for the Lambda calculus using Barendregt's variable convention in Constructive Type Theory (2017)
      Completo
      SZASZ, N , COPELLO, E. , TASISTRO, A.

      Evento: Internacional
      Descripción: 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017)
      Ciudad: Brasilia
      Año del evento: 2017
      Publicación arbitrada
      Palabras clave: Constructive Type Theory Lambda calculus Formal Metatheory
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
    • Dependent Types for Nominal Terms with Atom Substitutions (2015)
      Completo
      TASISTRO, A. , FEARWEATHER, E. , FERNÁNDEZ, M. , SZASZ, N

      Evento: Internacional
      Descripción: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
      Ciudad: Varsovia, Polonia
      Año del evento: 2015
      Anales/Proceedings:LIPIcs
      Volumen:38
      Pagina inicial: 180
      Pagina final: 195
      ISSN/ISBN: 1868-8969
      Publicación arbitrada
      Editorial: LIPIcs – Leibniz International Proceedings in Informatics
      Palabras clave: Nominal Abstract Syntax Dependent Type System
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
      http://drops.dagstuhl.de/opus/volltexte/lipics-complete/lipics-vol38-tlca2015-complete.pdf
    • Alpha-Induction and Recursion for the Lambda Calculus in Constructive Type Theory (2015)
      Completo
      COPELLO, E. , TASISTRO, A. , SZASZ, N , BOVE A. , FERNÁNDEZ, M.

      Evento: Internacional
      Descripción: Logical and Semantical Frameworks with Applications (LSFA 2015)
      Ciudad: Natal, Brasil
      Año del evento: 2015
      Anales/Proceedings:LSFA 2015 Proceedings
      Publicación arbitrada
      Palabras clave: Metateoría formal Cálculo Lambda Teoría Constructiva de Tipos
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
      https://www.mat.ufrn.br/~LSFA2015/preproceedings.pdf
    • Presentation of Classical Propositional Tableaux on Program Design Premises (2015)
      Completo
      TASISTRO, A. , MICHELINI, J.

      Evento: Internacional
      Descripción: 4th International Conference on Tools for Teaching Logic (TTL2015)
      Ciudad: Rennes, Francia
      Año del evento: 2015
      Publicación arbitrada
      Palabras clave: didáctica de la lógica
      Areas de conocimiento:
      Ciencias Sociales / Ciencias de la Educación / Educación General /
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
    • Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda (2014)
      Completo
      TASISTRO, A. , COPELLO, E. , BIANCHI B.

      Evento: Internacional
      Descripción: 18th Simpósio Brasileiro de Linguagens de Programação (SBLP 2014)
      Ciudad: Maceió, Alagoas, Brasil
      Año del evento: 2014
      Anales/Proceedings:Lecture Notes in Computer Science, Programming Languages, 18th. Brazilian Symposium, SBLP 2014
      Volumen:8771
      ISSN/ISBN: 0302-9743
      Publicación arbitrada
      Editorial: Springer
      Palabras clave: Dependently Typed Programming
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
      DOI: 10.1007/978-3-319-11863-5_5
      http://link.springer.com/chapter/10.1007%2F978-3-319-11863-5_5#page-1
    • Novel Didactic Proof Assistant for First-Order Logic Natural Deduction (2014)
      Completo
      PAIS, J. , TASISTRO, A.

      Evento: Internacional
      Descripción: First International Conference, LCT 2014, Held as Part of HCI International 2014.
      Ciudad: Heraklion, Crete, Greece.
      Año del evento: 2014
      Anales/Proceedings:Lecture Notes in Computer Science. Learning and Collaboration Technologies. Designing and Developing Novel Learning Experiences.
      Volumen:8523
      Pagina inicial: 441
      Pagina final: 451
      ISSN/ISBN: 0302-9743 / 97
      Publicación arbitrada
      Escrita por invitación
      Editorial: Springer International Publishing
      Palabras clave: Interactive Theorem Proving Tools for Teaching Logic
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación /
      Ciencias Sociales / Ciencias de la Educación / Educación General /
      Medio de divulgación: Papel
      DOI: 10.1007/978-3-319-07482-5_42
      http://link.springer.com/chapter/10.1007%2F978-3-319-07482-5_42
    • On a Style of Presentation of Type Systems (2014)
      Completo
      TASISTRO, A.

      Evento: Internacional
      Descripción: Federated Logic Conference
      Ciudad: Viena, Austria
      Año del evento: 2014
      Anales/Proceedings:FLoC 2014
      Publicación arbitrada
      Palabras clave: Type Theory
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Otros
    • Design and Implementation of a Proof Assistant for Natural Deduction (2012)
      Completo
      TASISTRO, A. , PAIS, J.

      Evento: Internacional
      Descripción: Simposio Internacional de Informática Educativa (SIIE 2012)
      Ciudad: Andorra La Vella, Andorra.
      Año del evento: 2012
      Palabras clave: educational software teaching logic formal proof
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
      Ciencias Sociales / Ciencias de la Educación / Educación General / Enseñanaza Universitaria
      Medio de divulgación: Papel
    • PSPDC : An Adaptation of the PSP to Incorporate Verified Design by Contract. (2012)
      Completo
      TASISTRO, A. , MORENO, S. , VALLESPIR, D.

      Evento: Internacional
      Descripción: TSP Symposium 2012
      Ciudad: St. Petersburg, Florida, USA
      Año del evento: 2012
      Anales/Proceedings:TSP Symposium 2012 Proceedings.
      Publicación arbitrada
      Editorial: Software Engineering Institute, Carnegie Mellon University.
      Ciudad: Pittsburgh, USA.
      Palabras clave: Personal Software Process Formal Methods (Verified) Design by Contract
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
      Medio de divulgación: Papel
    • A Type-Theoretic Framework for Certified Model Transformations (2011)
      Completo
      TASISTRO, A. , LUNA, C. , CALEGARI, D. , SZASZ, N

      Evento: Internacional
      Descripción: 13th Simpósio Brasileiro de Métodos Formais (SBMF 2010)
      Ciudad: Natal, Brasil
      Año del evento: 2011
      Anales/Proceedings:lecture Notes in Computer Science, 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers
      Volumen:6527
      Pagina inicial: 112
      Pagina final: 127
      ISSN/ISBN: 978-3-642-1982
      Editorial: Springer
      Palabras clave: Type Theory Model Transformations
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales de Ingeniería de Software
      Medio de divulgación: Papel
      DOI: 10.1007/978-3-642-19829-8_8
      http://link.springer.com/chapter/10.1007%2F978-3-642-19829-8_8
    • Experiment with a Type-Theoretic Approach to the Verification of Model Transformations (2009)
      Completo
      TASISTRO, A. , SZASZ, N , LUNA, C. , CALEGARI, D.

      Evento: Internacional
      Descripción: Jornadas Chilenas de Computación 2009
      Ciudad: Santiago de Chile
      Año del evento: 2009
      Publicación arbitrada
      Palabras clave: Ingeniería Dirigida por Modelos Teoría de Tipos Verificación Formal
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales en Ingeniería de Software
      Medio de divulgación: Papel
    • A Formal Semantics of Object-Oriented System State Modification Primitives (2004)
      Completo
      TASISTRO, A. , VIGNAGA, A.

      Evento: Internacional
      Descripción: Fist Conference on Principles of Software Engineering - PRISE 2004
      Ciudad: Buenos Aires
      Año del evento: 2004
      Anales/Proceedings:Fist Conference on Principles of Software Engineering
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Métodos Formales
      Medio de divulgación: Papel
    • Specification of a Smart Card Operating System (2000)
      Completo
      TASISTRO, A. , BETARTE, G , CORNES C. , SZASZ, N

      Evento: Internacional
      Descripción: TYPES 2000
      Ciudad: Durham, Inglaterra
      Año del evento: 2000
      Anales/Proceedings:Lecture Notes in Computer Science
      Volumen:1956
      Pagina inicial: 77
      Pagina final: 93
      ISSN/ISBN: 0302-9743
      Publicación arbitrada
      Editorial: Springer
      Palabras clave: Teoría de Tipos Métodos Formales de Ingeniería de Software
      Areas de conocimiento:
      Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones /
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
    • Abstract Insertion Sort in an Extension of Type Theory with Record Types and Subtyping (1998)
      Completo
      TASISTRO, A.

      Evento: Internacional
      Descripción: TYPES 1998
      Ciudad: Kloster Irsee
      Año del evento: 1998
      Anales/Proceedings:Lecture Notes in Computer Science
      Volumen:1512
      Pagina inicial: 354
      Pagina final: 372
      ISSN/ISBN: 0302-9743
      Publicación arbitrada
      Editorial: Springer
      Palabras clave: Type Theory Dependently Typed Programming
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      Medio de divulgación: Papel
    • A machine-assisted proof of the subject reduction property for a small typed functional language (1996)
      Completo
      BOVE, A , TASISTRO, A.

      Evento: Internacional
      Descripción: 3rd. Workshop on Logic, Language, Information and Computation (WoLLIC 96)
      Ciudad: Salvador
      Año del evento: 1996
      Anales/Proceedings:3rd. Workshop on Logic, Language, Information and Computation
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
      Medio de divulgación: Papel
    • Formalisation of systems of algebras using dependent record types and subtyping: an example (1995)
      Completo
      BETARTE, G , TASISTRO, A.

      Evento: Internacional
      Descripción: 7th. Nordic Workshop on Programming Theory
      Ciudad: Göteborg
      Año del evento: 1995
      Anales/Proceedings:Proceedings of the 7th. Nordic Workshop on Programming Theory
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
      Medio de divulgación: Papel
    • Dijkstra´s Methodology and Martin-Lof´s Type Theory (1990)
      Completo
      TASISTRO, A. , BOLLINI, S.

      Evento: Internacional
      Descripción: X Conferencia Internacional de la Sociedad Chilena de Ciencias de la Computación
      Ciudad: Santiago, Chile
      Año del evento: 1990
      Anales/Proceedings:X Conferencia Internacional de la Sociedad Chilena de Ciencias de la Computación
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
      Medio de divulgación: Papel
    • Un método de inferencia de tipos para programas lógicos (1989)
      Completo
      TASISTRO, A. , KESNER, D.

      Evento: Regional
      Descripción: XVIII Jornadas Argentinas de Informática e Investigación Operativa
      Ciudad: Buenos Aires, Argentina
      Año del evento: 1989
      Anales/Proceedings: XVIII Jornadas Argentinas de Informática e Investigación Operativa
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
      Medio de divulgación: Papel
    • Un sistema de tipos polimórfico para un lenguaje funcional con constantes y tipos abstractos (1988)
      Completo
      TASISTRO, A. , GASPES, V.

      Evento: Regional
      Descripción: XIV Conferencia Latinoamericana de Informática
      Ciudad: Buenos Aires, Argentina
      Año del evento: 1988
      Anales/Proceedings:XIV Conferencia Latinoamericana de Informática
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
      Medio de divulgación: Papel
    • Especificaciones algebraicas de tipos abstractos de datos en un curso medio de programación (1986)
      Completo
      TASISTRO, A. , VIOLA, A.

      Evento: Regional
      Descripción: XII Conferencia Latinoamericana de Informática
      Ciudad: Montevideo, Uruguay
      Año del evento: 1986
      Anales/Proceedings: XII Conferencia Latinoamericana de Informática
      Areas de conocimiento:
      Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación /
  • Producción técnica

    • Productos

      • Andy 1 1/2 (2013)
        Software, Otra
        TASISTRO, A. , PAIS, J.
        Asistente Didáctico de Demostración en Deducción Natural, Lógica de Primer Orden.
        País: Uruguay
        Disponibilidad: Irrestricta
        Palabras clave: software educacional enseñanza de Lógica
        Areas de conocimiento:
        Ciencias Sociales / Ciencias de la Educación / Educación General / Didáctica de la Lógica
        Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
        Medio de divulgación: Internet
        http://fi.ort.edu.uy/innovaportal/v/3641/5/fi.ort.front/inicio.html
      • Andy 0 (2010)
        Software, Otra
        PAIS, J. , TASISTRO, A.
        Asistente Didáctico de Demostración en Deducción Natural, Lógica Proposicional.
        País: Uruguay
        Disponibilidad: Irrestricta
        Producto con aplicación productiva o social: Uso en cursos de Lógica de la Universidad ORT Uruguay
        Palabras clave: software educacional enseñanza de Lógica
        Areas de conocimiento:
        Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
        Ciencias Sociales / Ciencias de la Educación / Educación General / Didáctica de la Lógica
        Medio de divulgación: Internet
        http://fi.ort.edu.uy/innovaportal/v/3641/5/fi.ort.front/inicio.html
      • SubRec (2002)
        Software, Otra
        TASISTRO, A. , BETARTE, G
        Asistente para el desarrollo y verificación de programas en la Teorí­a Constructiva de Tipos de Martin-Lof extendida con registros dependientes y subtipos
        País: Uruguay
        Disponibilidad: Irrestricta
        Institución financiadora: Proyecto CONICYT 4112
        Areas de conocimiento:
        Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
        Medio de divulgación: Internet
        http://www.fing.edu.uy/inco/grupos/mf/Proyectos/Investigacion/TTSUBOBJ/index.html
      • Fob (2001)
        Software, Otra
        TASISTRO, A. , BETARTE, G
        Intérprete de modelo de lenguaje orientado a objetos con métodos funcionales
        País: Uruguay
        Disponibilidad: Irrestricta
        Institución financiadora: Proyecto CONICYT 4112
        Areas de conocimiento:
        Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
        Medio de divulgación: Internet
        http://www.fing.edu.uy/inco/grupos/mf/Proyectos/Investigacion/TTSUBOBJ/index.html
      • GLICH (1997)
        Software, Otra
        CABEZAS, J , TASISTRO, A.
        Asistente para el desarrollo de programas de corrección certificada
        País: Uruguay
        Disponibilidad: Irrestricta
        Institución financiadora: Proyecto CONICYT-BID 043
        Areas de conocimiento:
        Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógicas de la programación
        Medio de divulgación: Internet
    • Evaluaciones

      • Evaluación de Proyectos

        • Evaluación independiente de proyectos

          STIC-AmSud ( 2015 )
          Francia
          INRIA
          Cantidad: Menos de 5
        • Fondo de CONACYT ( 2014 )
          Paraguay
          CONACYT
          Cantidad: Menos de 5
        • PICT ( 2011 / 2011 )
          Argentina
          PICT
          Cantidad: Menos de 5
          Investigaciones sobre la aleatoriedad algorítmica
        • CONICET ( 2009 / 2009 )
          Argentina
          CONICET
          Cantidad: Menos de 5
          Proyecto PICT Joven 2008 - Análisis automático de código orientado a objetos para la verificación e inferencia de propiedades.
      • Evaluación de Publicaciones

        • Comité editorial

          CLEI Electronic Journal ( 2011 / 2011 )

          Cantidad: Menos de 5
        • Lecture Notes In Computer Science - Vol 806: Types for proofs and programs ( 1993 / 1993 )

          Cantidad: Menos de 5
        • Revisiones

          CLEI Electronic Journal ( 2015 )
          Tipo de publicación: Revista
          Cantidad: Menos de 5
      • Evaluación de eventos y congresos

        • Logical and Semantical Frameworks with Applications ( 2014 / 2018 )
          Comité programa congreso
          Brasil
          Arbitrado


        • CIESC (Congreso Iberoamericano de Enseñanza Superior en Computación) ( 2013 )

          Venezuela


        • Concurso Latinoamericano de Tesis de Maestría CLEI ( 2011 )

          Ecuador


          Presidente del Comité de Programa.
        • CIESC (Congreso Iberoamericano de Enseñanza Superior en Computación) ( 2006 )

          Chile


        • CIESC (Congreso Iberoamericano de Enseñanza Superior en Computación) ( 2005 )

          Colombia


        • WAIT (Workshop Argentino de Informática Teórica) ( 1999 )

          Argentina


        • II Conferencia Latinoamericana de Programación Funcional ( 1997 )
          Comité programa congreso
          Argentina
          Arbitrado

          Universidad de Buenos Aires
        • Concurso de Tesis de Maestría CLEI-UNESCO ( 1997 / 2004 )
          Revisiones
          Uruguay


          Presidente del Comité de Programa
      • Evaluación de premios

        • Premio L'Oreal a Científicas ( 2015 )
          Comité de asignación de premios y concursos
          Uruguay

          Cantidad: Menos de 5
          L'Oreal
      • Jurado de tesis

        • Doctorado en Ciencia de la Computación ( 2017 )
          Jurado de mesa de evaluación de tesis
          Sector Extranjero/Internacional/Otros / Facultad de Matemática, Astronomía y Física. U. Nacional de Córdoba , Argentina
          Nivel de formación: Doctorado
        • Doctorado en Informática ( 2015 )
          Jurado de mesa de evaluación de tesis
          Sector Educación Superior/Público / Programa de Desarrollo de las Ciencias Básicas / Programa de Desarrollo de las Ciencias Básicas , Uruguay
    • Formación de RRHH

      • Tutorías concluidas

        • Posgrado

          • A machine-checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution. (2018)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Master en Ingeniería
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: Martín Copes
            País/Idioma: Uruguay, Inglés
            Palabras Clave: Metateoría formal Cálculo Lambda Teoría Constructiva de Tipos
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • On the formal meta-theory of the Lambda calculus and languages with binders (2017)
            Tesis de doctorado
            Sector Educación Superior/Público / Universidad de la República / Facultad de Ingeniería - UDeLaR , Uruguay
            Programa: Doctorado en Informática (UDELAR-PEDECIBA)
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: Ernesto Copello
            Medio de divulgación: Papel
            País/Idioma: Uruguay, Español
            Palabras Clave: Meta-theory of Programming Languages Constructive Type Theory
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación
          • Foundations for Mathematical Methodology (2016)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Master en Ingeniería
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Juan Michelini
            País/Idioma: Uruguay, Inglés
            Palabras Clave: Mathematical Methodology Proof Methods
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
          • Especificación y verificación formal de modelos de marcapasos como autómatas temporizados (2015)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Master en Ingeniería
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Pablo Damonte
            Medio de divulgación: Papel
            País/Idioma: Uruguay, Español
            Palabras Clave: Métodos Formales Sistemas de Tiempo Real
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales de Construcción de Software
          • Semántica e interpretación de lenguajes de modelado y transformación de modelos (2013)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Master en Ingeniería
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Nicolás Fornaro
            País/Idioma: Uruguay, Español
            Palabras Clave: Ingeniería Dirigida por Modelos Sistemas de tipos Lenguajes de Transformaciones de Modelos
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
            Se estudia el desarrollo y adaptación de sistemas de tipos para lenguajes de transformaciones de modelos, aplicables en el marco de la Ingeniería Dirigida por Modelos (ver líneas de investigación y relevancia de la producción).
          • Incorporación de Métodos Formales a PSP (2013)
            Tesis de maestria
            Sector Educación Superior/Público / Universidad de la República / Facultad de Ingeniería - UDeLaR , Uruguay
            Programa: Maestría en Informática (UDELAR-PEDECIBA)
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: Silvana Moreno
            Medio de divulgación: Papel
            País/Idioma: Uruguay, Español
            Palabras Clave: Métodos Formales
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales de Construcción de Software
          • Asistente de demostración en Deducción Natural para Lógica de Predicados (2013)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Maestría en Ingeniería
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Jorge Pais
            País/Idioma: Uruguay, Español
            Palabras Clave: nominal syntax educational software teaching logic formal proof
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones
            Ciencias Sociales / Ciencias de la Educación / Educación General / Enseñanza Universitaria
          • Inferencia de Tipos de Sesión (2012)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Maestría en Ingeniería
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: Ernesto Copello
            Medio de divulgación: Papel
            País/Idioma: Uruguay, Español
            Palabras Clave: Meta-theory of Programming Languages Constructive Type Theory
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación
          • Software Unit Testing Techniques: An Empirical Study (2012)
            Tesis de doctorado
            Sector Educación Superior/Público / Universidad de la República / Facultad de Ingeniería - UDeLaR , Uruguay
            Programa: Doctorado en Informática (UDELAR-PEDECIBA)
            Tipo de orientación: Asesor/Orientador
            Nombre del orientado: Diego Vallespir
            Medio de divulgación: Papel
            País/Idioma: Uruguay, Inglés
            Palabras Clave: Calidad de software Ingeniería de software empírica Técnicas de ensayo de software
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
          • Mejora de la calidad de los prototipos desarrollados en un contexto académico (2006)
            Tesis de maestria
            Sector Educación Superior/Público / Universidad de la República / Facultad de Ingeniería - UDeLaR , Uruguay
            Programa: Maestría en Informática (UDELAR-PEDECIBA)
            Tipo de orientación: Asesor/Orientador
            Nombre del orientado: Diego Vallespir
            Medio de divulgación: Internet
            País/Idioma: Uruguay, Español
            Web: http://www.fing.edu.uy/inco/pedeciba/bibliote/tesis/tesis-vallespir.pdf
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones
          • Una semántica formal de primitivas de modificación de estados de sistemas orientados a objetos (2004)
            Tesis de maestria
            Sector Educación Superior/Público / Universidad de la República / Facultad de Ingeniería - UDeLaR , Uruguay
            Programa: Maestría en Informática (UDELAR-PEDECIBA)
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Andrés Vignaga
            Medio de divulgación: Internet
            País/Idioma: Uruguay, Inglés
            Web: http://www.fing.edu.uy/inco/pedeciba/bibliote/tesis/tesis-vignaga.pdf
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Métodos Formales
          • A machine-assisted Proof of the subject reduction property for a small typed functional language (1995)
            Tesis de maestria
            Sector Educación Superior/Público / Universidad de la República / Facultad de Ingeniería - UDeLaR , Uruguay
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Ana Bove
            Medio de divulgación: Internet
            País/Idioma: Uruguay, Inglés
            Web: http://www.fing.edu.uy/inco/pedeciba/bibliote/tesis/tesis-bove.pdf
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Métodos Formales
        • Grado

          • Puerto de Shen para Erlang (2018)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería / Escuela de Ingeniería , Uruguay
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Sebastián Borrazás
            Medio de divulgación: CD-Rom
            País/Idioma: Uruguay, Español
            Palabras Clave: Lenguajes de programación Compiladores Verificación de programas
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lenguajes de Programación
          • Introducción a TLA+: Especificación de marcapasos (2018)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería / Escuela de Ingeniería , Uruguay
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Lorenzo Rodríguez
            Medio de divulgación: CD-Rom
            País/Idioma: Uruguay, Español
            Palabras Clave: Especificación formal de sistemas Lógica temporal
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales de Ingeniería de Software
          • OntoCIS: Ontología del currículo de Ingeniería en Sistemas (2018)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería / Escuela de Ingeniería , Uruguay
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Lucía Sarni
            Medio de divulgación: CD-Rom
            País/Idioma: Uruguay, Español
            Palabras Clave: Ontologías Ingeniería en Sistemas Currículos
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Ontologías
          • Especificación y Derivación Formal de Programas Imperativos (2018)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Nicolás Ferreira
            País/Idioma: Uruguay, Español
            Palabras Clave: Métodos Formales Métodos y Lenguajes de Programación
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Métodos Formales de Ingeniería de Software
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Lenguaje de especificación de formularios para ingreso y validación de datos (2018)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Emil Santurio
            País/Idioma: Uruguay, Español
            Palabras Clave: Lenguajes de dominio específico Especificación formal de Lenguajes de Programación Compiladores
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Lenguajes de Programación
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lenguajes de Programación
          • Piano virtual (2017)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: Mauricio Delbono y Christian Mangold
            Medio de divulgación: CD-Rom
            País/Idioma: Uruguay, Español
            Palabras Clave: Realidad virtual
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Realidad virtual
          • InterfLan: Interface Language. Lenguaje de especificación de interfaces para ingreso y validación de datos. (2017)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Licenciatura en Ingeniería de Software
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Emil Santurio y Joaquín Silveira
            País/Idioma: Uruguay, Español
            Palabras Clave: Lenguaje específico de dominio Lenguaje de especificación de interfaces
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Diseño e implementación de lenguajes de programación
          • Verificación formal de algoritmos de aplicación industrial (2016)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Guillermo Colmenero
            País/Idioma: Uruguay, Español
            Palabras Clave: Métodos Formales Verificación semi-automática de programas
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
          • Matemática de programas en cursos de Ingeniería de Software (2016)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Martín Copes
            País/Idioma: Uruguay, Español
            Palabras Clave: Lógica Programación Matemática Enseñanza en Ingeniería de Software
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
            Ciencias Sociales / Ciencias de la Educación / Educación General / Educación Superior
          • Duphly: Compositor automático de música. (2016)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Gastón Nieves y Juan Ignacio Zunino
            País/Idioma: Uruguay, Español
            Palabras Clave: Composición automática de música
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
          • Programación basada en invariantes: un enfoque didáctico. (2016)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Eitan Fogel y Alejandro Milieris
            País/Idioma: Uruguay, Español
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
            Ciencias Sociales / Ciencias de la Educación / Educación General / Didáctica de la programación
          • Assisi: Asistente de demostraciones en Deducción Natural para Lógica Esquemática de Primer Orden (2016)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Sebastián Urciuoli
            País/Idioma: Uruguay, Español
            Palabras Clave: Asistentes de demostración
            Areas de conocimiento:
            Ingeniería y Tecnología / Ingeniería Eléctrica, Ingeniería Electrónica e Ingeniería de la Información / Ingeniería de Sistemas y Comunicaciones / Ingeniería de Software
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Andy 1 1/2 : Asistente de composición de derivaciones esquemáticas en Deducción Natural de Primer Orden (2014)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Licenciatura en Ingeniería de Software
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Martín Copes, Gastón Nieves y Sebastián Urciuoli
            Medio de divulgación: CD-Rom
            País/Idioma: Uruguay, Español
            Palabras Clave: Proof Assistants Nominal techniques
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación
            Ciencias Sociales / Ciencias de la Educación / Educación General / Didáctica de la Lógica
          • Compositor de demostraciones calculacionales (2013)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Licenciatura en Análisis de Sistemas de Información
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Juan Michelini
            Medio de divulgación: Internet
            País/Idioma: Uruguay, Español
            Web: http://fi.ort.edu.uy/innovaportal/v/3641/5/fi.ort.front/inicio.html
            Palabras Clave: Mathematical Methodology Mechanical Theorem Proving
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
          • Suite de aplicaciones bioinformáticas (2013)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Licenciatura en Análisis de Sistemas de Información
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Federico Machado, Roque Giordano
            País/Idioma: Uruguay, Español
            Web: http://fi.ort.edu.uy/innovaportal/v/3641/5/fi.ort.front/inicio.html
            Palabras Clave: aplicaciones bioinformáticas
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Bioinformática
            El programa académico es: Licenciatura en Bioinformática, que no figura entre las opciones disponibles.
          • Asistente Didáctico de Demostraciones en Deducción Natural para Lógica de Primer Orden (2010)
            Tesis/Monografía de grado
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Ingeniería en Sistemas
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Jorge Pais
            Medio de divulgación: Papel
            País/Idioma: Uruguay, Español
            Palabras Clave: didáctica de la lógica deducción natural
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
      • Tutorías en marcha

        • Posgrado

          • Generación y verificación semi-automática de software paralelo usando trasnformaciones formales de programas (2018)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería / Escuela de Ingeniería , Uruguay
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: José Solsona
            País/Idioma: Uruguay, Español
            Palabras Clave: Programación concurrente Transformación de programas
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Teoría de la Programación
          • Formalizaciones de demostraciones de normalización del cálculo lambda con tipos simples en Teoría Constructiva de Tipos (2018)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Tipo de orientación: Cotutor en pie de igualdad
            Nombre del orientado: Sebastián Urciuoli
            País/Idioma: Uruguay, Inglés
            Palabras Clave: Demostración Interactiva de Teoremas Metateoría formal. Cálculo Lambda
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Programación con Tipos Dependientes (2017)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Maestría en Ingeniería
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Andrés Nieves
            País/Idioma: Uruguay, Español
            Palabras Clave: Teoría de Tipos Métodos y Lenguajes de Programación Tipos Dependientes
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
          • Composición musical semiautomática (2016)
            Tesis de maestria
            Sector Educación Superior/Privado / Universidad ORT Uruguay / Universidad ORT Uruguay - Facultad de Ingeniería , Uruguay
            Programa: Master en Ingeniería
            Tipo de orientación: Tutor único o principal
            Nombre del orientado: Gastón Nieves
            País/Idioma: Uruguay, Español
            Palabras Clave: Composición musical semiautomática
            Areas de conocimiento:
            Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación
    • Otros datos relevantes

      • Premios, Honores y Títulos

        • Premio a la Excelencia Docente (2015)
          (Nacional)
          Facultad de Ingeniería, Universidad ORT Uruguay.
          Se premia la trayectoria de docentes de la Facultad.
        • Mención Especial (1999)
          Premio Roberto Caldeyro Barcia para jóvenes investigadores

      • Presentaciones en eventos

        • Jornadas de Ciencia de la Computación (2015)
          Congreso
          Matemática y Programación en una carrera de Ingeniería de Software
          Argentina
          Tipo de participación: Conferencista invitado
          Carga horaria: 20
          Nombre de la institución promotora: Universidad Nacional de Rosario
          Palabras Clave: Currículos de Ingeniería de Software Enseñanza de Métodos Formales
          Areas de conocimiento:
          Ciencias Sociales / Ciencias de la Educación / Educación General / Currículos universitarios
        • Federated Logic Conference (FLoC 2014) (2014)
          Congreso
          Gentle Formalisation of Stoughton´s Substitution in Constructive Type Theory
          Austria
          Tipo de participación: Expositor oral
          Carga horaria: 40
          Nombre de la institución promotora: Universidad Tecnológica de Viena
          Palabras Clave: Metateoría formal Cálculo Lambda Teoría Constructiva de Tipos
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Computación Teórica
        • LSFA 2013 - Logical and Semantical Frameworks with Applications (2013)
          Congreso
          Proof Assistant for One-and-a-Halfth Order Logic
          Brasil
          Tipo de participación: Conferencista invitado
          Nombre de la institución promotora: Universidade de Sao Paulo
          Palabras Clave: Proof Assistants Interactive Theorem Proving
          Areas de conocimiento:
          Ciencias Naturales y Exactas / Ciencias de la Computación e Información / Ciencias de la Computación / Lógica
      • Construcción institucional

        Desde 2009 soy el coordinador académico de la Maestría en Ingeniería (por investigación) de la Universidad ORT Uruguay (http://fi.ort.edu.uy/postgrado)., un programa que cuenta con 20 egresados y al momento 15 estudiantes. Fui el redactor de su programa de estudios. Actualmente me encuentro en el proceso de confección de la propuesta y programa de estudios del Doctorado en Ciencias de la Ingeniería de la Universidad ORT Uruguay.

        En 2009 fui co-fundador y desde entonces co-dirijo el grupo CompuTe de investigación en Computación Teórica en la Universidad ORT Uruguay (http://fi.ort.edu.uy/grupo-de-computacion-teorica). En 2007 me hice cargo de la Cátedra de Teoría de la Computación de la Universidad ORT Uruguay, que actualmente cuenta con más de 40 docentes, la mayoría de ellos jóvenes ayudantes y asistentes con planes de desarrollo académico. Entre 1985 y 2000 cooperé en el desarrollo del InCo (Instituto de Computación, Universidad de la República).

    • Información adicional

      La tesis de maestría:
      Type Inference for Session Types
      de Ernesto Copello, co-orientada por mí y por Nora Szasz,
      recibió el Primer Premio del 20avo. Concurso Latinoamericano de Tesis de Maestría (CLEI 2013).
      A ese concurso se presentaron 48 tesis de toda Latinoamérica.
       

    • Indicadores de producción

      Producción bibliográfica

      38
      Artículos publicados en revistas científicas
      7
      Completo 7
      Trabajos en eventos
      23
      Libros y Capítulos
      2
      Libro publicado 1
      Capítulos de libro publicado 1
      Documentos de trabajo
      6
      Completo 6

      Producción técnica

      5
      Productos tecnológicos
      5

      Evaluaciones

      17
      Evaluación de proyectos
      4
      Evaluación de eventos
      8
      Evaluación de publicaciones
      3
      Jurado de tesis
      2

      Formación RRHH

      32
      Tutorías/Orientaciones/Supervisiones concluidas
      28
      Tesis de maestria 10
      Tesis/Monografía de grado 16
      Tesis de doctorado 2
      Tutorías/Orientaciones/Supervisiones en marcha
      4
      Tesis de maestria 4