Pedro Henrique Azevedo de Amorim

Possui graduação em Ciência da Computação - Ecole Polytechnique (2016), graduação em Engenharia de Computação pela Universidade Estadual de Campinas (2017), mestrado em Ciência da Computação - École Normale Supérieure de Cachan (2017) e doutorado em Ciência da Computação pela Cornell University (2023). Tem experiência na área de Ciência da Computação, com ênfase em Linguagens de Programação e Verificação Formal.

Informações coletadas do Lattes em 20/12/2025

Acadêmico

Formação acadêmica

Doutorado em Ciência da Computação

2018 - 2023

Cornell University
Título: A Unifying Semantics for Markov Kernels and Linear Operators
Orientador: Dexter Kozen
Grande área: Ciências Exatas e da TerraGrande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Linguagens de Programação.

Mestrado em Ciência da Computação

2016 - 2017

École Normale Supérieure de Cachan, ENS/Cachan
Título: Otimização matemática em Coq, Ano de Obtenção: 2017
Orientador: Adam Chlipala
Bolsista do(a): Institut national de recherche en informatique et en automatique, INRIA, França.

Graduação em Ciência da Computação

2014 - 2016

Ecole Polytechnique
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.

Graduação em Engenharia de Computação

2011 - 2017

Universidade Estadual de Campinas

Pós-doutorado

2023

Pós-Doutorado. , University of Oxford, OX, Inglaterra. , Grande área: Ciências Exatas e da Terra

Idiomas

Inglês

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Português

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Francês

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Áreas de atuação

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Linguagens de Programação.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Lógicas e Semântica de Programas.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Verificação Formal.

Participação em eventos

40th Conference on Mathematical Foundations of Programming Semantics. 2024. (Congresso).

ANR PPS 5th meeting.Compositional Expected Cost Semantics for Functional Probabilistic Programs. 2023. (Encontro).

European joint conferences on theory and practice of software. A Higher-Order Language for Markov Kernels and Linear Operators. 2023. (Congresso).

Languages for Inference 2023.Separated and Shared Effects in Higher-Order Languages. 2023. (Oficina).

49th ACM SIGPLAN Symposium on Principles of Programming Languages. 2022. (Congresso).

Workshop on Differentiable Programming. 2022. (Oficina).

2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).Universal Semantics for the Stochastics λ-Calculus. 2021. (Simpósio).

Joint PPS - PIHOC - DIAPASoN Workshop.Distribution Theoretic Semantics for Differentiable Programming. 2021. (Oficina).

44th ACM SIGPLAN Symposium on Principles of Programming Languages. 2017. (Congresso).

Produções bibliográficas

NIGAM, RACHIT ; AZEVEDO DE AMORIM, PEDRO HENRIQUE ; SAMPSON, ADRIAN . Modular Hardware Design with Timeline Types. Proceedings Of The Acm On Programming Languages-Pacmpl , v. 7, p. 343-367, 2023.
WEIRICH, STEPHANIE ; VOIZARD, ANTOINE ; DE AMORIM, PEDRO HENRIQUE AZEVEDO ; EISENBERG, RICHARD A. . A specification for dependent types in Haskell. Proceedings Of The Acm On Programming Languages-Pacmpl , v. 1, p. 1-29, 2017.
DE AMORIM, PEDRO H. AZEVEDO . A Higher-Order Language for Markov Kernels and Linear Operators. Lecture Notes in Computer Science. 1ed.: Springer Nature Switzerland, 2023, v. , p. 89-112.
AZEVEDO DE AMORIM, PEDRO H. ; KOZEN, DEXTER ; MARDARE, RADU ; PANANGADEN, PRAKASH ; ROBERTS, MICHAEL . Universal Semantics for the Stochastic λ-Calculus. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021, Rome. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021. p. 1.
HIRSCH, ANDREW K. ; AMORIM, PEDRO H. AZEVEDO DE ; CECCHETTI, ETHAN ; TATE, ROSS ; ARDEN, OWEN . First-Order Logic for Flow-Limited Authorization. In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF), 2020, Boston. 2020 IEEE 33rd Computer Security Foundations Symposium (CSF), 2020. p. 123.

Histórico profissional

Experiência profissional

2023 - Atual

University of Oxford

Vínculo: Research associate, Enquadramento Funcional: Research associate, Carga horária: 40, Regime: Dedicação exclusiva.

2017 - 2017

Massachusetts Institute Of Technology

Vínculo: Visiting student, Enquadramento Funcional: Estagiário de pesquisa, Carga horária: 40, Regime: Dedicação exclusiva.

2016 - 2016

University of Pennsylvania

Vínculo: Visiting student, Enquadramento Funcional: Estagiário de pesquisa, Carga horária: 40, Regime: Dedicação exclusiva.

2015 - 2015

I-Systems

Vínculo: PROGRAMA DE ESTÁGIO, Enquadramento Funcional: Estagiário, Carga horária: 30, Regime: Dedicação exclusiva.