Diferencia entre revisiones de «Temas»
De Seminario de Lógica Computacional (2018)
(→Temas de Seminario de lógica computacional (2018)) |
(→Temas de Seminario de lógica computacional (2018)) |
||
| Línea 7: | Línea 7: | ||
*** [http://www.seas.upenn.edu/~cis500/current/lectures/lec01.pdf Introducción de B. Pierce al curso "Software foundations"]. | *** [http://www.seas.upenn.edu/~cis500/current/lectures/lec01.pdf Introducción de B. Pierce al curso "Software foundations"]. | ||
*** [https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html Introducción del libro "Software foundations"]. | *** [https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html Introducción del libro "Software foundations"]. | ||
| − | ** Tema 1: [[https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html | + | ** Tema 1: [[https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html Programación funcional en Coq]] ([[Tema 1 | Código]]). |
| − | ** Tema 2: [[https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html | + | ** Tema 2: [[https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html Demostraciones por inducción en Coq ([[Tema 2 | Código]]). |
| − | ** Tema 3: [[https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html | + | ** Tema 3: [[https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html Datos estructurados en Coq]] ([[Tema 3 | Código]]). |
| − | ** Tema 4: [[https://softwarefoundations.cis.upenn.edu/lf-current/Poly.html | + | ** Tema 4: [[https://softwarefoundations.cis.upenn.edu/lf-current/Poly.html Polimorfismo y orden superior en Coq]] ([[Tema 4 | Código]]). |
| − | ** Tema 5: [[https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html | + | ** Tema 5: [[https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html Tácticas básicas]] ([[Tema 5 | Código]]). |
* Programación lógica | * Programación lógica | ||
Revisión del 11:10 6 may 2018
Temas de Seminario de lógica computacional (2018)
En esta página se irán publicando los temas conforme se vayan estudiando.
- Demostración asistida por ordenador con Coq
- Tema 0: Introducción al Seminario
- Tema 1: [Programación funcional en Coq] ( Código).
- Tema 2: [[https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html Demostraciones por inducción en Coq ( Código).
- Tema 3: [Datos estructurados en Coq] ( Código).
- Tema 4: [Polimorfismo y orden superior en Coq] ( Código).
- Tema 5: [Tácticas básicas] ( Código).
- Programación lógica
Ponentes
- Ponentes de las próximas sesiones:
- Samuel Ortiz Morales
- Borja Sierra Miranda
- Ponentes de las sesiones anteriores:
- Ángel Ruiz Campos (Tema 1)
- Alejandro Rodríguez Rodríguez (Tema 2)
- Jorge Catarecha Otero-Saavedra (Tema 3)
- Miriam Medrán Navarro (Tema 4).
Participantes
Los participantes en el Seminario son
- Alejandro Rodriguez Rodríguez
- Ángel Ruiz Campos
- Borja Sierra Miranda
- Elías Guisado Villalgordo
- Jorge Catarecha Otero-Saavedra
- Marina Jiménez Comez
- Mencía Veas Lerdo de Tejada
- Samuel Ortiz Morales