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 para o paradigma quântico;
- fundamentos, métodos e ferramentas para a especificação e verificação de programas quânticos.
Programa
- Categorias para a computação quântica
- Processos, categorias e diagramas.
- Categorias, funtores e transformações naturais.
- Propriedades universais e adjunções.
- Categorias monoidais; Aplicações: (categorias de) relações, matrizes e espaços de Hilbert.
- Processos quânticos
- Categorias monoidais e raciocínio diagramático.
- 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).
- Teoria dos processos quânticos.
- Lógicas computacionais para a computação quântica
- O que é uma lógica? Lógica e computação: lógica intuicionista, modal e linear.
- O lambda-calculus linear e a correspondência de Curry-Howard para a computação quântica. Variantes.
- Modelação e verificação de algoritmos quânticos.
Apoio
Notas de Apoio (2018-19)
- A hands-on introduction to categories (Luis S. Barbosa)
Artigos de referência
- Introduction to Categories and Categorical Logic (S. Abramsky and N. Tzevelekos, 2011)
- Physics, Topology, Logic and Computation: A Rosetta Stone (J. Baez and M. Stay, 2011)
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. Introduction to categories and categorical logic. 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.09.28