Mário Florido is an Associate Professor at FCUP (Faculty of Science, University of Porto). His main research interests include the design and definition of novel type systems for the Lambda-Calculus and Functional Programming Languages. He supervised several PhD thesis on this area, and colaborated on several research projects, either as researcher and a principal researcher. He has several publications on the major conferences of the area, such as ICFP, ESOP, PPDP, PADL and CSL, and major journals such as TCS, JFP, TPLP, JAR and JLC. He is also member of top international research networks on the area of Type Systems for Programming languages, such as EUTYPES and TACLe.
Alves, S., Dundua, B., Florido, M. and Kutsia, T. (2018). Pattern-based calculi with finitary matching. Logic Journal of the IGPL, 26 (2), pp. 203–243
Jost, S., Vasconcelos, P., Florido, M. and Hammond, K. (2017). Type-Based Cost Analysis for Lazy Functional Languages. Journal of Automated Reasoning
Nigam, V. and Florido, M. (2017). Preface. Electr. Notes Theor. Comput. Sci., 332, pp. 1–2
Silva, M., Florido, M. and Pfenning, F. (2016). Non-Blocking Concurrent Imperative Programming with Session Types. LINEARITY (pp. 64–72)
Dundua, B., Florido, M., Kutsia, T. and Marin, M. (2016). \emphCLP(H): Constraint logic programming for hedges. TPLP, 16 (2), pp. 141–162
Vasconcelos, P., Jost, S., Florido, M. and Hammond, K. (2015). Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. PROGRAMMING LANGUAGES AND SYSTEMS (pp. 787-811)
Dundua, B., Florido, M. and Kutsia, T. (2015). Lambda Calculus with Regular Types. SYNASC (pp. 129–136)
Dundua, B., Florido, M., Kutsia, T. and Marin, M. (2015). CLP(H): Constraint Logic Programming for Hedges. CoRR, abs/1503.00336
Rodrigues, V., Akesson, B., Florido, M., de Sousa, S., Pedroso, J. and Vasconcelos, P. (2015). Certifying execution time in multicores. SCIENCE OF COMPUTER PROGRAMMING, 111 (P3), pp. 505-534
Amaral, C., Florido, M. and Costa, V. S. (2014). PrologCheck - Property-Based Testing in Prolog. FLOPS (pp. 1–17)
Pereira, M., Alves, S. and Florido, M. (2014). Liquid Intersection Types. ITRS (pp. 24–42)
Florido, M. and Mackie, I. (2014). Linearity in Computation. J. Log. Comput., 24 (3), pp. 511–512
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2014). Linearity: A Roadmap. J. Log. Comput., 24 (3), pp. 513–529
Dundua, B., Florido, M., Kutsia, T. and Marin, M. (2014). Constraint Logic Programming for Hedges: A Semantic Reconstruction. FLOPS (pp. 285–301)
Rodrigues, V., Akesson, B., Sousa, S. and Florido, M. (2013). A Declarative Compositional Timing Analysis for Multicores Using the Latency-Rate Abstraction. Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings (pp. 43-59)
Rodrigues, V., Pedroso, J., Florido, M. and De Sousa, S. (2012). Certifying execution time. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 108-125)
Simoes, H., Vasconcelos, P., Florido, M., Jost, S. and Hammond, K. (2012). Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. ACM SIGPLAN NOTICES, 47 (9), pp. 165-176
Coelho, J. and Florido, M. (2011). Semantic Verification in an Open Collaboration Scenario. Future Information Technology (pp. 44-53)
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2011). Linearity and recursion in a typed Lambda-calculus. PPDP (pp. 173–182)
Amaral, C., Florido, M. and Jansson, P. (2011). Interfacing dynamically typed languages and the why tool: reasoning about lists and tuples. Erlang Workshop (pp. 92–93)
Rodrigues, V., Pedroso, J. P., Florido, M. and de Sousa, S. M. (2011). Certifying Execution Time. FOPARA (pp. 108–125)
Rodrigues, V., Florido, M. and de Sousa, S. (2011). A Functional Approach to Worst-Case Execution Time Analysis. FUNCTIONAL AND CONSTRAINT LOGIC PROGRAMMING (pp. 86-103)
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2010). Linearity and iterator types for Gödel’s System. Higher-Order and Symbolic Computation, 23 (1), pp. 1–27
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2010). Linear Recursion. CoRR, abs/1001.3368
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2010). Gödel’s system tau revisited. Theor. Comput. Sci., 411 (11-13), pp. 1484–1500
Coelho, J., Dundua, B., Florido, M. and Kutsia, T. (2010). A Rule-Based Approach to XML Processing and Web Reasoning. RR (pp. 164–172)
Coelho, J., Florido, M. and Kutsia, T. (2009). Collaborative Schema Construction using Regular Sequence Types. IRI (pp. 290–295)
Coelho, J. and Florido, M. (2008). XCentric: Constraint based XML Processing. Proceedings of XML: Applications and Associated Technologies (XATA 2008) (pp. 64)
Coelho, J., Florido, M. and Kutsia, T. (2008). Sequence Disunification and one Application to Collaborative Schema Construction. Days in Logic
Alves, S., Florido, M., Mackie, I. and Sinot, F. (2008). Minimality in a Linear Calculus with Iteration. Electr. Notes Theor. Comput. Sci., 204, pp. 163–179
Coelho, J. and Florido, M. (2007). XCentric: logic programming for XML processing. WIDM (pp. 1–8)
Coelho, J. and Florido, M. (2007). XCentric: A Logic-Programming Language for XML Processing. PLAN-X (pp. 93–94)
Simoes, H., Hammond, K., Florido, M. and Vasconcelos, P. (2007). Using intersection types for cost-analysis of higher-order polymorphic functional programs. TYPES FOR PROOFS AND PROGRAMS (pp. 221-236)
Coelho, J. and Florido, M. (2007). Type-Based Static and Dynamic Website Verification. ICIW (pp. 32)
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2007). The Power of Closed Reduction Strategies. Electr. Notes Theor. Comput. Sci., 174 (10), pp. 57–74
Coelho, J., Florido, M. and Kutsia, T. (2007). Sequence Disunification and Its Application in Collaborative Schema Construction. WISE Workshops (pp. 91–102)
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2007). Linear Recursive Functions. Rewriting, Computation and Proof (pp. 182–195)
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2007). Iterator Types. FoSSaCS (pp. 17–31)
Coelho, J. and Florido, M. (2006). VeriFLog: A Constraint Logic Programming Approach to Verification of Website Content. APWeb Workshops (pp. 148–156)
Simões, H. R., Hammond, K., Florido, M. and Vasconcelos, P. B. (2006). Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. TYPES (pp. 221–236)
Coelho, J. and Florido, M. (2006). Unification with flexible arity symbols: a typed approach. UNIF06: 20th International Workshop on Unification, pp. 74
Alves, S., Fernández, M., Florido, M. and Mackie, I. (2006). The Power of Linear Functions. CSL (pp. 119–134)
Coelho, J. and Florido, M. (2005). XML PRocessing in Logic Programming. XATA2005, XML: Aplicações e Tecnologias Associadas (Vila Verde, Braga, 10 e 11 de Fevereiro de 2005)
Alves, S. and Florido, M. (2005). Weak linearization of the lambda calculus. Theor. Comput. Sci., 342 (1), pp. 79–103
Florido, M. and Damas, L. (2004). Linearization of the lambda-calculus and its relation with intersection type systems. J. Funct. Program., 14 (5), pp. 519–546
Coelho, J. and Florido, M. (2004). CLP(Flex): Constraint Logic Programming Applied to XML Processing. CoopIS/DOA/ODBASE (2) (pp. 1098–1112)
Coelho, J. and Florido, M. (2003). Type-Based XML Processing in Logic Programming. PADL (pp. 273–285)
Alves, S. and Florido, M. (2003). Linearization by Program Transformation. LOPSTR (pp. 160–175)
Alves, S. and Florido, M. (2002). Type Inference using Constraint Handling Rules. Electr. Notes Theor. Comput. Sci., 64, pp. 56–72
Dundua, B. (2014). Programming with Sequence and Context Variables: Foundations and Applications. (Doctoral dissertation, Faculty of Sciences, University of Porto)
Simões, H. (2014). Amortised Resource Analysis for Lazy Functional Programs. (Doctoral dissertation, Faculty of Sciences, University of Porto)
Rodrigues, V. (2013). Semantics-based Program Verification: an Abstract Interpretation Approach. (Doctoral dissertation, Faculty of Sciences, University of Porto)
Coelho, J. (2007). XML Processing in Logic Programming. (Doctoral dissertation, Faculty of Sciences, University of Porto)
Alves, S. (2007). Linearisation of the Lambda-Calculus. (Doctoral dissertation, Faculty of Sciences, University of Porto)
