Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
TEORIA DEI TIPI
SCP6076357, A.A. 2017/18

Informazioni valide per gli studenti immatricolati nell'A.A. 2017/18

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2017/18
N0
porta questa
pagina con te
Crediti formativi 6.0
Tipo di valutazione Voto
Denominazione inglese TYPE THEORY
Sito della struttura didattica http://informatica.scienze.unipd.it/2017/laurea_magistrale
Dipartimento di riferimento Dipartimento di Matematica
Obbligo di frequenza No
Lingua di erogazione ITALIANO
Sede PADOVA
Corso singolo È possibile iscriversi all'insegnamento come corso singolo
Corso a libera scelta È possibile utilizzare l'insegnamento come corso a libera scelta

Docenti
Responsabile GIOVANNI SAMBIN
Altri docenti MARIA EMILIA MAIETTI MAT/01

Dettaglio crediti formativi
Tipologia Ambito Disciplinare Settore Scientifico-Disciplinare Crediti
AFFINE/INTEGRATIVA Attività formative affini o integrative MAT/01 6.0

Organizzazione dell'insegnamento
Periodo di erogazione Secondo semestre
Anno di corso I Anno
Modalità di erogazione frontale

Tipo ore Crediti Ore di
didattica
assistita
Ore Studio
Individuale
LEZIONE 6.0 48 102.0

Calendario
Inizio attività didattiche 26/02/2018
Fine attività didattiche 01/06/2018
Visualizza il calendario delle lezioni Lezioni 2018/19 Ord.2014

Commissioni d'esame
Commissione Dal Al Membri
3 a.a. 2018/2019 01/10/2018 28/02/2020 MAIETTI MARIA EMILIA (Presidente)
CIRAULO FRANCESCO (Membro Effettivo)
SAMBIN GIOVANNI (Membro Effettivo)
BONOTTO CINZIA (Supplente)
MASCHIO SAMUELE (Supplente)

Syllabus
Prerequisiti: E' caldamente suggerito, ma non strettamente necessario, aver seguito un corso di introduzione alla logica matematica.
Conoscenze e abilita' da acquisire: 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).
Modalita' di esame: L'accertamento di profitto avverrà con una prova orale dopo il completamento di esercitazioni personali da parte dello studente.
Criteri di valutazione: 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.
Contenuti: 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).
Attivita' di apprendimento previste e metodologie di insegnamento: Lezioni frontali e laboratorio.
Eventuali indicazioni sui materiali di studio: Appunti forniti dal docente.
Testi di riferimento:
  • 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. Cerca nel catalogo