Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
FONDAMENTI LOGICI DEI LINGUAGGI FUNZIONALI
SC03119888, A.A. 2015/16

Informazioni valide per gli studenti immatricolati nell'A.A. 2015/16

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2015/16
N0
porta questa
pagina con te
Crediti formativi 6.0
Tipo di valutazione Voto
Denominazione inglese LOGICAL FOUNDATIONS OF FUNCTIONAL LANGUAGES
Sito della struttura didattica http://informatica.scienze.unipd.it/2015/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 SILVIO VALENTINI
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
ESERCITAZIONE 1.0 8 17.0
LEZIONE 5.0 40 85.0

Calendario
Inizio attività didattiche 01/03/2016
Fine attività didattiche 15/06/2016
Visualizza il calendario delle lezioni Lezioni 2019/20 Ord.2014

Commissioni d'esame
Nessuna commissione d'esame definita

Syllabus
Prerequisiti: Conoscenze di base di logica matematica e del linguaggio insiemistico
Conoscenze e abilita' da acquisire: Lo scopo di questo corso è quello di fornire una introduzione teorica ai linguaggi di programmazione funzionali tipati e non tipati.
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: Dopo aver richiamato la nozione di funzione calcolabile si introdurrà il lambda calcolo puro e si dimostrerà che esso è uno strumento universale di calcolo. Si analizzerà quindi il lambda calcolo tipato semplice ed i suoi legami con il frammento implicativo del calcolo proposizionale intuizionista. Si introdurrano poi il calcolo con tipi dipendenti, che rappresenta il contenuto computazionale della logica del primo ordine, per continuare con calcoli con tipi di secondo ordine, potenti quanto l'aritmetica di Heyting al secondo ordine, e finire quindi con calcoli estremamente potenti che considerano insieme entrambi i sistemi di tipi ed eventualmente anche i tipi induttivamente generati, i tipi ricorsivi ed i tipi intersezione. Per tutti tali lambda calcoli si intendono dimostrare i principali teoremi matematici, vale a dire il teorema di normalizzazione e di confluenza e di validita' in opportune semantiche denotazionali, e fornire esempi di applicazione in informatica teorica.
Attivita' di apprendimento previste e metodologie di insegnamento: Lezioni frontali in aula
Eventuali indicazioni sui materiali di studio: Appunti forniti dal docente
Testi di riferimento:
  • J.Y.Girard, Y.Lafont, P.Taylor, Proofs and Types. --: Cambridge University Press, --. Cerca nel catalogo
  • H.Barendreght, The Lambda Calculus, its Syntax and Semantics. --: North-Holland, --. Cerca nel catalogo
  • H.Barendreght,, Lambda Calculi with Types. --: Oxford University Press, --. Handbook of Logic in Computer Science Cerca nel catalogo