% introductionCENIDET
\documentclass[xcolor=dvipsnames,svgnames,prologue]{beamer}

\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}
\usepackage{amscd,amsfonts,amsmath,amssymb,latexsym,enumerate,textcomp,listings,proof}
\usepackage{url}

\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}

%\mode<presentation>

\title{Perfil}
\author{José de Jesús Lavalle Martínez\inst{1} 
}
\institute[BUAP]{
\url{http://www.aleteya.cs.buap.mx/~jlavalle} \\
\texttt{jlavallenator@gmail.com} \\
\inst{1}Facultad de Ciencias de la Computación \\
Benemérita Universidad Autónoma de Puebla
}
\date[CENIDET]{24 de Octubre de 2011 \\ 
Centro Nacional de Investigación y Desarrollo Tecnológico}


\usetheme{Madrid}
\usecolortheme[named=Brown]{structure}


\begin{document}

\begin{frame}
\titlepage
\end{frame}

\begin{frame}
\frametitle{Contenido}
\tableofcontents[pausesections]
\end{frame}

\section{Docencia}

\begin{frame}
\frametitle{Área de Conocimiento: Teoría de la Computación}
\begin{itemize}[<+->]
\item Lógica Matemática (Clásica);
\item Demostración Automática de Teoremas (Sistemas de Gentzen Libres de Corte);
\item Computabilidad (Máquinas URM y Funciones Recursivas);
\item Lenguajes Formales y Autómatas (Desde Autómatas Finitos hasta Máquinas de Turing);
\item Métodos Formales (Chequeo de Modelos);
\item Fundamentos de Lenguajes de Programación (Semántica Operacional);
\item Lenguajes de Programación (Programación Declarativa: Lógica y Funcional).
\end{itemize}
\end{frame}

\section{Áreas de interés}

\begin{frame}
\frametitle{Intereses}
\begin{itemize}
\item<1> Métodos Formales;
\item<2> Especificación y Verificación Formal;
\item<3> Demostración Automática de Teoremas.
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Tesis Dirigidas}
\begin{enumerate}
\item<6-> La Semántica de Acción para el Lenguaje PCF;
\item<3-> Caracterización de Redes de Petri y Sistemas de Reescritura de 
Términos mediante Reescritura Regulada;
\item<1-> Especificación Formal de un Sistema de Recuperación de Información
Modelado con UML;
\item<5-> Especificación Formal de Sistemas Distribuidos mediante Cálculo-$\pi$;
\item<4-> Especificación y Verificación de Circuitos Lógicos mediante el Álgebra de
Procesos Circal;
\item<6-> Semántica Denotacional del Modelo de Actores;
\item<3-> Redes de Petri para la Especificación de Sistemas Concurrentes;
\item<2-> Intérprete de ML y Demostración Automática de Teoremas en Lógica de Alto
Orden;
\item<1-> Prototipo para la Notación Z;
\item<2-> Especificación Formal de Sistemas Interactivos mediante Lógica Lineal.
\end{enumerate}
\end{frame}


\section{Intereses Actuales}
\begin{frame}
\frametitle{Trabajos en Proceso}
\begin{itemize}[<+->]
\item PACO: demostrador autómatico para lógica proposicional PAraCOnsistente (Sistema de Gentzen Libre de Corte para $C_\omega$ inspirado en $NCG_\omega$); 
\item Chequeo de modelos (Autómatas de Büchi, Lógica de Tiempo Lineal, SPIN) para sistemas que se comunican asíncronamente.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Trabajos por Iniciar}
\begin{itemize}[<+- | alert@+>]
\item Ontologías; 
\item Lógica Descriptiva;
\item Pellet (el Principal Sistema de Razonamiento para OWL).
\end{itemize}
\end{frame}

\section{Cierre}
\begin{frame}
\frametitle{Finalmente,}\pause
\begin{center}
{\Huge ¡Muchas gracias!}
\end{center}
\end{frame}

\end{document}