Types for Proofs and Programs

"Tipi per Prove e Programmi" è una raccolta di contributi selezionati e sottoposti a revisione, presentati nell'ambito del workshop annuale del progetto TYPES. Questo workshop si è svolto dal 26 al 29 marzo 2008 a Torino, Italia, e ha riunito oltre 100 ricercatori che si occupano di metodi formali e programmazione informatica basata sulla teoria dei tipi. Gli argomenti trattati includono, tra l'altro, linguaggi di programmazione, strumenti informatici per la dimostrazione formale e le loro applicazioni in vari settori come l'analisi dei linguaggi di programmazione, il software certificato e la matematica formale. I contributi sono stati selezionati da 27 lavori presentati, sottoposti a un rigoroso processo di revisione. I curatori, Stefano Berardi, Ferruccio Damiani e Ugo De Liguoro, hanno garantito la qualità e la rilevanza dei lavori per fornire un contributo prezioso alla discussione scientifica in questo campo.