???global.info.a_carregar???
Mário Florido concluiu o Doutoramento em Ciência de Computadores em 1998 pela Universidade do Porto, Faculdade de Ciências, e o MSc em Foundations of Advanced Information Technology em 1991 pelo Imperial College London. É Professor Associado na Universidade do Porto, Faculdade de Ciências. Publicou vários artigos em revistas e conferências especializadas. Atua na área de Ciências da Computação e da Informação com ênfase nas áreas de Modelos de Computação e Programação Funcional. No seu currículo Ciência Vitae os termos mais frequentes na contextualização da produção científica e tecnológica são: Lambda-calculus; Sistemas de Tipos; Haskell; .
Ler resumo completo ↓
Identificação

Identificação pessoal

Nome completo
Mário Florido

Nomes de citação

  • Florido, Mário

Identificadores de autor

Ciência ID
121B-522B-5B55
ORCID iD
0000-0002-0574-7555

Endereços de correio eletrónico

  • amf@dcc.fc.up.pt (Profissional)
  • amflorid@fc.up.pt (Profissional)

Websites

  • https://sigarra.up.pt/fcup/pt/func_geral.FormView?P_CODIGO=238703 (Profissional)

Domínios de atuação

  • Ciências Exatas - Ciências da Computação e da Informação - Ciências da Computação
Formação
Grau Classificação
1998
Concluído
 Doutoramento em Ciência de Computadores (Doutoramento)
Especialização em Ciência de Computadores
Universidade do Porto Faculdade de Ciências, Portugal
"Sistemas de Tipos para Linguagens Declarativas" (TESE/DISSERTAÇÃO)
 aprovado por unanimidade
1991
Concluído
 Foundations of Advanced Information Technology (Master)
Imperial College London Department of Computing, Reino Unido
"A Constraint Solver fo IC-Prolog II" (TESE/DISSERTAÇÃO)
 Pass
1989
Concluído
 Matemática Aplicada (ramo de Ciência de Computadores) (Licenciatura)
Universidade do Porto Faculdade de Ciências, Portugal
"n/a" (TESE/DISSERTAÇÃO)
Percurso profissional

Docência no Ensino Superior

Categoria Profissional
Instituição de acolhimento 		Empregador
2010/03/17 - Atual Professor Associado (Docente Universitário) Universidade do Porto Faculdade de Ciências, Portugal
1998/02/11 - 2010/03/17 Professor Auxiliar (Docente Universitário) Universidade do Porto Faculdade de Ciências, Portugal
1995/09/01 - 1998/01/10 Assistente (Docente Universitário) Universidade do Minho Escola de Engenharia, Portugal
Projetos

Projeto

Designação Financiadores
2016 - 2019/08/01 Elven - Lógicas para verificação de programas na Web
PTDC/EEI-CTP/3506/2014
Investigador responsável
Universidade do Porto Faculdade de Ciências, Portugal

Instituto de Engenharia de Sistemas e Computadores, Portugal

Instituto de Telecomunicações, Portugal
Fundação para a Ciência e a Tecnologia
Concluído
2008 - 2011/03/31 JEDI - Um Ambiente Híbrido para Dedução e Indução - e a sua Aplicação sobre Dados Espaciais
PTDC/EIA/66924/2006
Investigador
Universidade do Porto Faculdade de Ciências, Portugal

Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores, Portugal

Universidade de Évora, Portugal

Universidade do Porto Instituto de Ciências e Tecnologias Agrárias e Agro-Alimentares, Portugal
Fundação para a Ciência e a Tecnologia
Concluído
2008 - 2011/03/31 RESCUE, Execução Fiável e Segura de Programas em Sistemas Embebidos
PTDC/EIA/65862/2006
Investigador
Universidade do Porto Faculdade de Ciências, Portugal

Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores, Portugal

Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto, Portugal

Universidade do Minho, Portugal

Universidade da Beira Interior, Portugal
Fundação para a Ciência e a Tecnologia
Concluído
Produções

Publicações

Artigo em conferência
  1. Akama, S.; Nakayama, Y.. "A three-valued semantics for Typed Logic Programming". Trabalho apresentado em ICLP Technical Communications, 2019.
    10.1109/ismvl.1995.513520
  2. Florido, Mário; Pedro Ângelo. "Type Inference for Rank 2 Gradual Intersection Types". Trabalho apresentado em The symposium on Trends in Functional Programming (TFP), 2019.
    Aceite para publicação
  3. Dundua, B; Florido, M; Kutsia, T. "Lambda Calculus with Regular Types". 2016.
    10.1109/synasc.2015.29
  4. Vasconcelos, P; Jost, S; Florido, M; Hammond, K. "Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages". 2015.
    10.1007/978-3-662-46669-8_32
  5. Dundua, B; Florido, M; Kutsia, T; Marin, M. "Constraint Logic Programming for Hedges: A Semantic Reconstruction". 2014.
    10.1007/978-3-319-07151-0_18
  6. Amaral, C; Florido, M; Costa, VS. "PrologCheck - Property-Based Testing in Prolog". 2014.
    10.1007/978-3-319-07151-0_1
  7. Rodrigues, Vitor; Akesson, Benny; Sousa, SimaoMelode; Florido, Mario. "A Declarative Compositional Timing Analysis for Multicores Using the Latency-Rate Abstraction". 2013.
    10.1007/978-3-642-45284-0_4
  8. Rodrigues, V; Florido, M; de Sousa, SM. "A Functional Approach to Worst-Case Execution Time Analysis". 2011.
    10.1007/978-3-642-22531-4_6
  9. Coelho, J; Florido, M; Kutsia, T. "Collaborative Schema Construction using Regular Sequence Types". 2008.
    10.1109/iri.2009.5211567
  10. Coelho, J; Florido, M. "Type-based static and dynamic website verification". 2007.
    10.1109/iciw.2007.67
  11. Alves, S; Florido, M. "Type inference using constraint handling rules". 2002.
    10.1016/s1571-0661(04)80346-3
Artigo em revista
  1. Alves, S; Dundua, B; Florido, M; Kutsia, T. "Pattern-based calculi with finitary matching". LOGIC JOURNAL OF THE IGPL (2018):
    10.1093/jigpal/jzx059
  2. Silva, M; Florido, M; Pfenning, F. "Non-Blocking Concurrent Imperative Programming with Session Types". ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE (2017):
    10.4204/eptcs.238.7
  3. Jost, S; Vasconcelos, P; Florido, M; Hammond, K. "Type-Based Cost Analysis for Lazy Functional Languages". JOURNAL OF AUTOMATED REASONING (2017):
    10.1007/s10817-016-9398-9
  4. DUNDUA, B; FLORIDO, M; KUTSIA, T; MARIN, M. "CLP(H): Constraint logic programming for hedges". THEORY AND PRACTICE OF LOGIC PROGRAMMING (2016):
    10.1017/s1471068415000071
  5. Rodrigues, V; Akesson, B; Florido, M; de Sousa, SM; Pedroso, JP; Vasconcelos, P. "Certifying execution time in multicores". SCIENCE OF COMPUTER PROGRAMMING (2015):
    10.1016/j.scico.2015.06.006
  6. Pereira, M; Alves, S; Florido, M. "Liquid Intersection Types". ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE (2015):
    10.4204/eptcs.177.3
  7. Alves, S; Fernandez, M; Florido, M; Mackie, I. "Linearity: A Roadmap". JOURNAL OF LOGIC AND COMPUTATION (2014):
    10.1093/logcom/exs020
  8. Rodrigues, V.; Pedroso, J.P.; Florido, M.; De Sousa, S.M.. "Certifying execution time". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7177 LNCS (2012): 108-125. http://www.scopus.com/inward/record.url?eid=2-s2.0-84864655874&partnerID=MN8TOARS.
    10.1007/978-3-642-32495-6_7
  9. Simoes, H; Vasconcelos, P; Florido, M; Jost, S; Hammond, K. "Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs". ACM SIGPLAN NOTICES (2012):
    10.1145/2398856.2364575
  10. Simões, H.; Vasconcelos, P.; Florido, M.; Jost, S.; Hammond, K.. "Automatic amortised analysis of dynamic memory allocation for lazy functional programs". Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP (2012): 165-176. http://www.scopus.com/inward/record.url?eid=2-s2.0-84867491922&partnerID=MN8TOARS.
    10.1145/2364527.2364575
  11. Amaral, C.; Florido, M.; Jansson, P.. "Interfacing dynamically typed languages and the why tool: Reasoning about lists and tuples". Erlang'11 - Proceedings of the 2011 ACM SIGPLAN Erlang Workshop (2011): 92-93. http://www.scopus.com/inward/record.url?eid=2-s2.0-80755180991&partnerID=MN8TOARS.
    10.1145/2034654.2034673
  12. Alves, S.; Fernandez, M.; Florido, M.; Mackie, I.. "Linearity and recursion in a typed Lambda-Calculus". PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming (2011): 173-182. http://www.scopus.com/inward/record.url?eid=2-s2.0-80052153042&partnerID=MN8TOARS.
    10.1145/2003476.2003500
  13. Coelho, J.; Florido, M.. "Semantic verification in an open collaboration scenario". Communications in Computer and Information Science 185 CCIS PART 2 (2011): 44-53. http://www.scopus.com/inward/record.url?eid=2-s2.0-79960149872&partnerID=MN8TOARS.
    10.1007/978-3-642-22309-9_6
  14. Alves, S.; Fernández, M.; Florido, M.; MacKie, I.. "Linearity and iterator types for Gödel's System I". Higher-Order and Symbolic Computation 23 1 (2010): 1-27. http://www.scopus.com/inward/record.url?eid=2-s2.0-80051787315&partnerID=MN8TOARS.
    10.1007/s10990-010-9060-x
  15. Coelho, J.; Dundua, B.; Florido, M.; Kutsia, T.. "A rule-based approach to XML processing and web reasoning". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6333 LNCS (2010): 164-172. http://www.scopus.com/inward/record.url?eid=2-s2.0-78049414563&partnerID=MN8TOARS.
    10.1007/978-3-642-15918-3_13
  16. Alves, S.; Fernández, M.; Florido, M.; Mackie, I.. "Gödel's system T revisited". Theoretical Computer Science 411 11-13 (2010): 1484-1500. http://www.scopus.com/inward/record.url?eid=2-s2.0-76449111366&partnerID=MN8TOARS.
    10.1016/j.tcs.2009.11.014
  17. Coelho, J.; Florido, M.; Kutsia, T.. "Collaborative schema construction using regular sequence types". 2009 IEEE International Conference on Information Reuse and Integration, IRI 2009 (2009): 290-295. http://www.scopus.com/inward/record.url?eid=2-s2.0-70449375137&partnerID=MN8TOARS.
    10.1109/IRI.2009.5211567
  18. Alves, S.; Florido, M.; Mackie, I.; Sinot, F.-R.. "Minimality in a Linear Calculus with Iteration". Electronic Notes in Theoretical Computer Science 204 C (2008): 163-179. http://www.scopus.com/inward/record.url?eid=2-s2.0-41649088788&partnerID=MN8TOARS.
    10.1016/j.entcs.2008.03.060
  19. Alves, S.; Fernández, M.; Florido, M.; Mackie, I.. "Iterator types". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4423 LNCS (2007): 17-31. http://www.scopus.com/inward/record.url?eid=2-s2.0-37149026320&partnerID=MN8TOARS.
    10.1007/978-3-540-71389-0_3
  20. Coelho, J.; Florido, M.. "Type-based static and dynamic website verification". Second International Conference on Internet and Web Applications and Services, ICIW'07 (2007): http://www.scopus.com/inward/record.url?eid=2-s2.0-34548730303&partnerID=MN8TOARS.
    10.1109/ICIW.2007.67
  21. Alves, S.; Fernández, M.; Florido, M.; Mackie, I.. "The Power of Closed Reduction Strategies". Electronic Notes in Theoretical Computer Science 174 10 SPEC. I (2007): 57-74. http://www.scopus.com/inward/record.url?eid=2-s2.0-34347262687&partnerID=MN8TOARS.
    10.1016/j.entcs.2007.02.047
  22. Coelho, J.; Florido, M.. "XCentric: Logic programming for XML processing". International Conference on Information and Knowledge Management, Proceedings (2007): 1-8. http://www.scopus.com/inward/record.url?eid=2-s2.0-77951138379&partnerID=MN8TOARS.
    10.1145/1316902.1316904
  23. Simões, H.R.; Hammond, K.; Florido, M.; Vasconcelos, P.. "Using intersection types for cost-analysis of higher-order polymorphic functional programs". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4502 LNCS (2007): 221-236. http://www.scopus.com/inward/record.url?eid=2-s2.0-38049171024&partnerID=MN8TOARS.
  24. Alves, S.; Fernández, M.; Florido, M.; Mackie, I.. "Linear recursive functions". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4600 LNCS (2007): 182-196. http://www.scopus.com/inward/record.url?eid=2-s2.0-38149101148&partnerID=MN8TOARS.
    10.1007/978-3-540-73147-4_9
  25. Coelho, J.; Florido, M.; Kutsia, T.. "Sequence disunification and its application in collaborative schema construction". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4832 LNCS (2007): 91-102. http://www.scopus.com/inward/record.url?eid=2-s2.0-38149103157&partnerID=MN8TOARS.
  26. Alves, S.; Fernández, M.; Florido, M.; Mackie, I.. "The power of linear functions". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4207 LNCS (2006): 119-134. http://www.scopus.com/inward/record.url?eid=2-s2.0-33750294691&partnerID=MN8TOARS.
    10.1007/11874683_8
  27. Coelho, J.; Florido, M.. "VeriFLog: A constraint logic programming approach to verification of website content". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3842 LNCS (2006): 148-156. http://www.scopus.com/inward/record.url?eid=2-s2.0-33745644505&partnerID=MN8TOARS.
  28. Alves, S.; Florido, M.. "Weak linearization of the lambda calculus". Theoretical Computer Science 342 1 (2005): 79-103. http://www.scopus.com/inward/record.url?eid=2-s2.0-23844478588&partnerID=MN8TOARS.
    10.1016/j.tcs.2005.06.005
  29. Alves, S.; Florido, M.. "Linearization by program transformation". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3018 (2004): 160-175. http://www.scopus.com/inward/record.url?eid=2-s2.0-33645251909&partnerID=MN8TOARS.
    10.1007/978-3-540-25938-1_14
  30. Coelho, J.; Florido, M.. "CLP (Flex): Constraint logic programming applied to XML processing". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3291 (2004): 1098-1112. http://www.scopus.com/inward/record.url?eid=2-s2.0-35048902431&partnerID=MN8TOARS.
  31. Florido, M.; Damas, L.. "Linearization of the lambda-calculus and its relation with intersection type systems". Journal of Functional Programming 14 5 (2004): 519-546. http://www.scopus.com/inward/record.url?eid=2-s2.0-4444368533&partnerID=MN8TOARS.
    10.1017/S0956796803004970
  32. Coelho, J.; Florido, M.. "Type-based XML processing in logic programming". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2562 (2003): 273-285. http://www.scopus.com/inward/record.url?eid=2-s2.0-33846115452&partnerID=MN8TOARS.
Atividades

Orientação

Título / Tema
Papel desempenhado 		Curso (Tipo)
Instituição / Organização
2018/11 - Atual Type Assignment in Logic Programming
Orientador de João Barbosa
 Doutoramento em Ciência de Computadores (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2018/11 - Atual Gradual Intersection Types
Orientador de Pedro Ângelo
 Doutoramento em Ciência de Computadores (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2011/05 - 2014/09 Programmimg with Sequence and Context Variables: Foundations and Applications
Orientador de Besik Dundua
 Doutoramento em Ciência de Computadores (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2005/09 - 2014/02 Amortised Resource Analysis for Lazy Functional Programs
Orientador de Hugo Simões
 Doutoramento em Ciência de Computadores (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2009/07 - 2013/05 Semantics-based Program Verification: an Abstract Interpretation Approach
Orientador de Vítor Rodrigues
 MAPI - MAP Doctoral Program in Computer Science (Doutoramento)
Universidade do Porto, Portugal
2004/07 - 2007/11 XML Processing in Logic Programming
Orientador de Jorge Coelho
 Doutoramento em Ciência de Computadores (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2002/10 - 2007/07 Linearisation of the Lambda-Calculus
Orientador de Sandra Alves
 Doutoramento em Ciência de Computadores da Faculdade de Ciências da Universidade do Porto (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal

Comissão de avaliação

Descrição da atividade
Tipo de assessoria 		Instituição / Organização Entidade financiadora
2014 - 2014 Membro do Painel de Avaliação de Candidaturas a Bolsas de doutoramento e pós-doutoramento FCT da área de Ciências da Computação e Informação
Avaliador
 Fundação para a Ciência e a Tecnologia, Portugal Fundação para a Ciência e a Tecnologia

Membro de comissão

Descrição da atividade
Tipo de participação 		Instituição / Organização
2019 - Atual Membro da direção do Laboratório em Inteligência Artificial e Ciência de Computadores da Universidade do Porto (LIACC)
Membro
 Universidade do Porto, Portugal
2017/01/01 - Atual Member of the Management Committee of the European research network on types for programming and verification (EUTypes) - CA15123
Membro
 European Union, Bélgica
2010/09 - 2014/09 Vice-presidente do conselho executivo do Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto
Presidente / Vice-presidente
 Universidade do Porto Faculdade de Ciências, Portugal