Objectivos e Resultados de Aprendizagem
O desenvolvimento da informação e computação quânticas requer ferramentas formais que permitam raciocinar rigorosamente sobre sistemas quânticos. Esta unidade curricular explora a ligação entre a computação (quântica) e as lógicas (sensíveis aos recursos) dada pela correspondência de Curry-Howard — que identifica proposições com tipos e provas com programas — e a ligação à semântica formalizada como uma categoria (monoidal). Assim, no final, os alunos serão capazes de aplicar ao desenvolvimento de programas quânticos um conhecimento sólido e operativo em
- semântica da programação e cálculos de programas no paradigma quântico;
- fundamentos, métodos e ferramentas para a especificação e verificação de programas quânticos.
Programa
- Fundamentos: modelos semânticos categoriais
- Categorias e propriedades universais.
- Functores e transformações naturais.
- Construções numa categoria.
- Adjunções; limites e colimites.
- Categorias cartesianas fechadas e categorias monoidais; Aplicações: (categorias de) relações, matrizes e espaços de Hilbert..
- Lógicas computacionais e semântica para a computação quântica
- O que é uma lógica? Lógica e computação: lógica intuicionista, modal e linear.
- Interpretação computacional dos postulados básicos da mecânica quântica; Estruturas categoriais correspondentes: monoidal (composição), compacta fechada (entanglement), adjunções (produto interno), biprodutos (ramificação não determinística).
- O lambda-calculus linear e a correspondência de Curry-Howard para a computação quântica. Variantes.
- Raciocínio diagramáticos para a derivação e modelação de algoritmos quânticos.
- Modelação e verificação de algoritmos quânticos em QUANTOMATIC e GLOBULAR.
Apoio
Notas de Apoio (2017-18)
Exercícios
Bibliografia base
- B. Coecke and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning . Cambridge University Press, 2017.
- S. Abramsky and B. Coecke. Categorical quantum mechanics . In Kurt Engesser, Dov Gabbay, and Daniel Lehmann, editors, Handbook of Quantum Logic and Quantum Structures, pages 261–324. North-Holland, Elsevier, 2011.
- S. Abramsky and N. Tzevelekos.i Introduction to categories and categorical logici . In B. Coecke, editor, New Structures for Physics, pages 3–94. Springer Lecture Notes on Physics (813), 2011.
Bibliografia complementar
- S. Awodey. Category Theory . Oxford Logic Guides. Oxford University Press, 2006.
Links
Funcionamento
Docente
Avaliação
- Provas de caracter individual (de realização não presencial)
Contacto
- Atendimento: Quarta 10-12 (por marcação)
- Email: lsb arroba di ponto uminho ponto pt
- Última actualização: 2018.03.22