\documentclass[a4paper,11pt]{article}
\usepackage {a4wide}

\begin{document}

\begin{itemize}
\item University, Pittsburgh, logic 
\item ce stage s'incrit dans le  cadre du projet manifest security
\item exemple des portes de bureau à CMU
\item formalisation de l'authorization avec une logique
\item le but est de construire des preuves dans cette logique
\item representation d'une preuve par un arbre
\item les feuilles sont les axiomes
\item les règles d'inferences seront les noeuds de l'arbre
\item on dit que le connecteur says est l'internalisation du jugement
\item l'avantage de cette logique est que ce que dit quelqu'un que l'on ne
connait pas ne nous influence pas
\item idée de ce que proof carrying architecture veut dire
\item logique indécidable
\item les ressources sont surveiller par un resource monitor
\end{itemize}

\textit{5 minutes}
transition ML5 

\begin{itemize}
\item notre travaille seras basé sur ML5
\item on part d'une logique pour définir le language
\item dans cette logique on distingue plusieurs mondes
\item signification de la boite, du diamant, du at
\item les règles correspondent au règles habituelles de la 
deduction naturelle
\item pour definir le language on définit des termes de preuve
(contienent toutes l'information nécessaire pour retrouver la preuve)
\end{itemize}

\textit{10 minutes}
transition Pcml5
\begin{itemize}

\end{itemize}


\end{document}
