Presentazione

Organizzazione della Didattica

DM270
INFORMATICA ORD. 2014


6

Corsi comuni

 

Frontali Esercizi Laboratorio Studio Individuale
ORE: 48 0 0 94

Periodo

AnnoPeriodo
I anno2 semestre

Frequenza

Facoltativa

Erogazione

Convenzionale

Lingua

Italiano

Calendario Attività Didattiche

InizioFine
26/02/201801/06/2018

Tipologia

TipologiaAmbitoSSDCFU
affine/integrativo Nessun ambitoMAT/016


Responsabile Insegnamento

ResponsabileSSDStruttura
Prof. SAMBIN GIOVANNIMAT/01Dipartimento di Matematica

Altri Docenti

DocenteCoperturaSSDStruttura
Prof.ssa MAIETTI MARIA EMILIAIstituzionaleMAT/01Dipartimento di Matematica

Attività di Supporto alla Didattica

Non previste.

Bollettino

E' caldamente suggerito, ma non strettamente necessario, aver seguito un corso di introduzione alla logica matematica.

Lo scopo di questo corso è quello di fornire una introduzione teorica alla teoria dei tipi per poter apprezzare le sue applicazioni in informatica (correttezza dei programmi funzionali e loro verifica in proof-assistant) e in matematica (sviluppo di prove costruttive con eventuale verifica formale al calcolatore ed estrazione del loro contenuto computazionale).

Lezioni frontali e laboratorio.

Nel corso verranno introdotti i principali concetti di teoria dei tipi al fine di apprezzarne alcune rilevanti applicazioni in ambito matematico, informatico e anche filosofico. Lo studente verra' introdotto a comprendere i seguenti aspetti della sua multiforme natura: 1) La natura computazionale della teoria dei tipi vista come lambda-calcolo tipato a' la Church che la rende un paradigma di un linguaggio di programmazione funzionale, in quanto permette di tipare i programmi con la loro specifica e di verificarne la correttezza in modo interattivo per mezzo di un proof-assistant. 2) La natura insiemistica della teoria dei tipi che la rende adatta a formalizzare le dimostrazioni in matematica costruttiva in modo da estrarne il contenuto computazionale. 3) La natura predicativa delle costruzioni di tipo dipendenti a' la Martin-Löf tramite generazione induttiva. Verranno illustrati esempi di costruzioni non predicative tramite l'utilizzo di paradossi. 4) La possibilità di presentare versioni intensionali o estensionali della teoria dei tipi al fine di enucleare importanti proprietà di decidibilità del type-checking utili a costruire un proof-assistant affidabile che permetta di formalizzare le prove matematiche in modo interattivo. Il corso includerà una parte in laboratorio che introdurrà gli studenti all'utilizzo di un proof-assistant ( il francese Coq o il bolognese Matita).

L'accertamento di profitto avverrà con una prova orale dopo il completamento di esercitazioni personali da parte dello studente.

L'esame intende valutare le conoscenze acquisite dallo studente sui temi del corso e le sue capacità di svolgere del lavoro autonomo su di essi.

Bengt Nordström, Kent Petersson, Jan M. Smith, Programming in Martin-Loef's Type Theory. : Oxford Uiniversity Press, 1990 P. Martin-Löf, Intuitionistic type theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. : Bibliopolis, 1984

Appunti forniti dal docente.