###### Algoritmi | User | António Mário Silva Marcos Florido

António Mário Silva Marcos Florido

António Mário Silva Marcos Florido

At LASI

Other with Dr Habil

Member of the LIACC R&D Unit

Academic Degree

Dr Habil

Current Position

at

Personal Webpage

Personal Email

amflorid@fc.up.ptOrcid

0000-0002-0574-7555Researcher ID

FCT Public Key

Ciência ID

121B-522B-5B55Google Scholar

About Me

Publications (68)

**Execution time program verification with tight bounds**

**Practical Aspects of Declarative Languages (PADL)**

2023 | conference-paper

**Execution Time Program Verification with Tight Bounds**

**Practical Aspects of Declarative Languages - 25th International Symposium, PADL 2023, Boston, MA, USA, January 16-17, 2023, Proceedings**

2023 | conference-paper

**A Typed Lambda Calculus with Gradual Intersection Types**

**PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20 - 22, 2022**

2022 | conference-paper

**Data Type Inference for Logic Programming**

**LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2021)**

2022 | conference-paper

**Execution Time Program Verification With Tight Bounds**

**CoRR**

2022 | journal-article

**Linear Rank Intersection Types**

**28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France**

2022 | conference-paper

**Structural Rules and Algebraic Properties of Intersection Types**

**Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings**

2022 | conference-paper

**Type Inference for Rank-2 Intersection Types Using Set Unification**

**Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings**

2022 | conference-paper

**Typed SLD-Resolution: Dynamic Typing for Logic Programming**

**LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2022)**

2022 | conference-paper

**Data Type Inference for Logic Programming**

**CoRR**

2021 | other

**Resource Analysis for Lazy Evaluation with Polynomial Potential**

**IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages, Virtual Event / Canterbury, UK, September 2-4, 2020**

2020 | conference-paper

**A Three-Valued Semantics for Typed Logic Programming**

**Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, September 20-25, 2019.**

2019 | conference-paper

**Type Inference for Rank 2 Gradual Intersection Types**

**The symposium on Trends in Functional Programming (TFP) **

2019 | conference-paper

**Type Inference for Rank 2 Gradual Intersection Types**

**Trends in Functional Programming - 20th International Symposium, TFP 2019, Vancouver, BC, Canada, June 12-14, 2019, Revised Selected Papers**

2019 | conference-paper

**Gradual Intersection Types**

**ITRS 2018: Ninth Workshop on Intersection Types and Related Systems**

2018 | conference-paper

**Pattern-based calculi with finitary matching**

**LOGIC JOURNAL OF THE IGPL**

2018 | journal-article

**Closed Types for Logic Programming**

**25TH INTERNATIONAL WORKSHOP ON FUNCTIONAL AND LOGIC PROGRAMMING**

2017 | conference-paper

**Type-Based Cost Analysis for Lazy Functional Languages**

**Journal of Automated Reasoning**

2017 | journal-article

**11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Porto, Portugal, January 1, 2016**

**LSFA**

2017 | edited-book

**Non-Blocking Concurrent Imperative Programming with Session Types**

**ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE**

2017 | journal-article

**Preface**

**Electronic Notes in Theoretical Computer Science**

2017 | other

**Type-Based Cost Analysis for Lazy Functional Languages**

**JOURNAL OF AUTOMATED REASONING**

2017 | journal-article

**CLP(H): Constraint logic programming for hedges**

**THEORY AND PRACTICE OF LOGIC PROGRAMMING**

2016 | journal-article

**Lambda Calculus with Regular Types**

**2015 17TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC)**

2016 | conference-paper

**Preface**

**11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Porto, Portugal, January 1, 2016**

2016 | conference-paper

**CLP(H): Constraint Logic Programming for Hedges**

**CoRR**

2015 | other

**Certifying execution time in multicores**

**SCIENCE OF COMPUTER PROGRAMMING**

2015 | journal-article

**Liquid Intersection Types**

**ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE**

2015 | journal-article

**Preface**

**Electronic Proceedings in Theoretical Computer Science, EPTCS**

2015 | other

**Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages**

**PROGRAMMING LANGUAGES AND SYSTEMS**

2015 | conference-paper

**Constraint Logic Programming for Hedges: A Semantic Reconstruction**

**FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2014**

2014 | conference-paper

**Linearity in Computation**

**J. Log. Comput.**

2014 | journal-article

**Linearity: A Roadmap**

**JOURNAL OF LOGIC AND COMPUTATION**

2014 | journal-article

**PrologCheck - Property-Based Testing in Prolog**

**FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2014**

2014 | conference-paper

**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**

2013 | conference-paper

**Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs**

**ACM SIGPLAN NOTICES**

2012 | journal-article

**Automatic amortised analysis of dynamic memory allocation for lazy functional programs**

**Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP**

2012 | journal-article

**Certifying execution time**

**Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)**

2012 | journal-article

**A Functional Approach to Worst-Case Execution Time Analysis**

**FUNCTIONAL AND CONSTRAINT LOGIC PROGRAMMING**

2011 | conference-paper

**Interfacing dynamically typed languages and the why tool: Reasoning about lists and tuples**

**Erlang'11 - Proceedings of the 2011 ACM SIGPLAN Erlang Workshop**

2011 | journal-article

**Linearity and recursion in a typed Lambda-Calculus**

**PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming**

2011 | journal-article

**Semantic verification in an open collaboration scenario**

**Communications in Computer and Information Science**

2011 | journal-article

**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)**

2010 | journal-article

**Gödel's system T revisited**

**Theoretical Computer Science**

2010 | journal-article

**Linear Recursion**

**CoRR**

2010 | other

**Linearity and iterator types for Gödel's System ℐ**

**Higher-Order and Symbolic Computation**

2010 | journal-article

**Preface**

**Electronic Proceedings in Theoretical Computer Science, EPTCS**

2010 | other

**Collaborative schema construction using regular sequence types**

**2009 IEEE International Conference on Information Reuse and Integration, IRI 2009**

2009 | journal-article

**Proceedings First International Workshop on Linearity, LINEARITY 2009, Coimbra, Portugal, 12th September 2009**

**LINEARITY**

2009 | edited-book

**Minimality in a Linear Calculus with Iteration**

**Electronic Notes in Theoretical Computer Science**

2008 | journal-article

**Iterator types**

**Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)**

2007 | journal-article

**Linear recursive functions**

2007 | journal-article

**Sequence disunification and its application in collaborative schema construction**

2007 | journal-article

**The Power of Closed Reduction Strategies**

**Electronic Notes in Theoretical Computer Science**

2007 | journal-article

**Type-based static and dynamic website verification**

**Second International Conference on Internet and Web Applications and Services, ICIW'07**

2007 | journal-article

**Using intersection types for cost-analysis of higher-order polymorphic functional programs**

2007 | journal-article

**XCentric: A Logic-Programming Language for XML Processing**

**PLAN-X 2007, Programming Language Technologies for XML, An ACM SIGPLAN Workshop colocated with POPL 2007, Nice, France, January 20, 2007**

2007 | conference-paper

**XCentric: Logic programming for XML processing**

**International Conference on Information and Knowledge Management, Proceedings**

2007 | journal-article

**The power of linear functions**

2006 | journal-article

**Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs**

**Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers**

2006 | conference-paper

**VeriFLog: A constraint logic programming approach to verification of website content**

2006 | journal-article

**Weak linearization of the lambda calculus**

**Theoretical Computer Science**

2005 | journal-article

**CLP (Flex): Constraint logic programming applied to XML processing**

2004 | journal-article

**Linearization by program transformation**

2004 | journal-article

**Linearization of the lambda-calculus and its relation with intersection type systems**

**Journal of Functional Programming**

2004 | journal-article

**Type-based XML processing in logic programming**

2003 | journal-article

**On the Relation between Rank 2 Intersection Types and Simple Types**

**AGP 2002: Proceedings of the Joint Conference on Declarative Programming, APPIA-GULP-PRODE, Madrid, Spain, September 16-18, 2002.**

2002 | conference-paper

**Type inference using constraint handling rules**

**Electronic Notes in Theoretical Computer Science**

2002 | journal-article

**Execution time program verification with tight bounds**

**Practical Aspects of Declarative Languages (PADL)**

2023 | conference-paper

**Execution Time Program Verification with Tight Bounds**

**Practical Aspects of Declarative Languages - 25th International Symposium, PADL 2023, Boston, MA, USA, January 16-17, 2023, Proceedings**

2023 | conference-paper

**A Typed Lambda Calculus with Gradual Intersection Types**

**PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20 - 22, 2022**

2022 | conference-paper

**Data Type Inference for Logic Programming**

**LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2021)**

2022 | conference-paper

**Execution Time Program Verification With Tight Bounds**

**CoRR**

2022 | journal-article

**Linear Rank Intersection Types**

**28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France**

2022 | conference-paper

**Structural Rules and Algebraic Properties of Intersection Types**

**Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings**

2022 | conference-paper

**Type Inference for Rank-2 Intersection Types Using Set Unification**

2022 | conference-paper

**Typed SLD-Resolution: Dynamic Typing for Logic Programming**

**LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2022)**

2022 | conference-paper

**Data Type Inference for Logic Programming**

**CoRR**

2021 | other

**Resource Analysis for Lazy Evaluation with Polynomial Potential**

**IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages, Virtual Event / Canterbury, UK, September 2-4, 2020**

2020 | conference-paper

**A Three-Valued Semantics for Typed Logic Programming**

**Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, September 20-25, 2019.**

2019 | conference-paper

**Type Inference for Rank 2 Gradual Intersection Types**

**The symposium on Trends in Functional Programming (TFP) **

2019 | conference-paper

**Type Inference for Rank 2 Gradual Intersection Types**

**Trends in Functional Programming - 20th International Symposium, TFP 2019, Vancouver, BC, Canada, June 12-14, 2019, Revised Selected Papers**

2019 | conference-paper

**Gradual Intersection Types**

**ITRS 2018: Ninth Workshop on Intersection Types and Related Systems**

2018 | conference-paper

**Pattern-based calculi with finitary matching**

**LOGIC JOURNAL OF THE IGPL**

2018 | journal-article

**Closed Types for Logic Programming**

**25TH INTERNATIONAL WORKSHOP ON FUNCTIONAL AND LOGIC PROGRAMMING**

2017 | conference-paper

**Type-Based Cost Analysis for Lazy Functional Languages**

**Journal of Automated Reasoning**

2017 | journal-article

**11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Porto, Portugal, January 1, 2016**

**LSFA**

2017 | edited-book

**Non-Blocking Concurrent Imperative Programming with Session Types**

**ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE**

2017 | journal-article

**Preface**

**Electronic Notes in Theoretical Computer Science**

2017 | other

**Type-Based Cost Analysis for Lazy Functional Languages**

**JOURNAL OF AUTOMATED REASONING**

2017 | journal-article

**CLP(H): Constraint logic programming for hedges**

**THEORY AND PRACTICE OF LOGIC PROGRAMMING**

2016 | journal-article

**Lambda Calculus with Regular Types**

**2015 17TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC)**

2016 | conference-paper

**Preface**

2016 | conference-paper

**CLP(H): Constraint Logic Programming for Hedges**

**CoRR**

2015 | other

**Certifying execution time in multicores**

**SCIENCE OF COMPUTER PROGRAMMING**

2015 | journal-article

**Liquid Intersection Types**

**ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE**

2015 | journal-article

**Preface**

**Electronic Proceedings in Theoretical Computer Science, EPTCS**

2015 | other

**Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages**

**PROGRAMMING LANGUAGES AND SYSTEMS**

2015 | conference-paper

**Constraint Logic Programming for Hedges: A Semantic Reconstruction**

**FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2014**

2014 | conference-paper

**Linearity in Computation**

**J. Log. Comput.**

2014 | journal-article

**Linearity: A Roadmap**

**JOURNAL OF LOGIC AND COMPUTATION**

2014 | journal-article

**PrologCheck - Property-Based Testing in Prolog**

**FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2014**

2014 | conference-paper

**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**

2013 | conference-paper

**Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs**

**ACM SIGPLAN NOTICES**

2012 | journal-article

**Automatic amortised analysis of dynamic memory allocation for lazy functional programs**

**Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP**

2012 | journal-article

**Certifying execution time**

2012 | journal-article

**A Functional Approach to Worst-Case Execution Time Analysis**

**FUNCTIONAL AND CONSTRAINT LOGIC PROGRAMMING**

2011 | conference-paper

**Interfacing dynamically typed languages and the why tool: Reasoning about lists and tuples**

**Erlang'11 - Proceedings of the 2011 ACM SIGPLAN Erlang Workshop**

2011 | journal-article

**Linearity and recursion in a typed Lambda-Calculus**

**PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming**

2011 | journal-article

**Semantic verification in an open collaboration scenario**

**Communications in Computer and Information Science**

2011 | journal-article

**A rule-based approach to XML processing and web reasoning**

2010 | journal-article

**Gödel's system T revisited**

**Theoretical Computer Science**

2010 | journal-article

**Linear Recursion**

**CoRR**

2010 | other

**Linearity and iterator types for Gödel's System ℐ**

**Higher-Order and Symbolic Computation**

2010 | journal-article

**Preface**

**Electronic Proceedings in Theoretical Computer Science, EPTCS**

2010 | other

**Collaborative schema construction using regular sequence types**

**2009 IEEE International Conference on Information Reuse and Integration, IRI 2009**

2009 | journal-article

**Proceedings First International Workshop on Linearity, LINEARITY 2009, Coimbra, Portugal, 12th September 2009**

**LINEARITY**

2009 | edited-book

**Minimality in a Linear Calculus with Iteration**

**Electronic Notes in Theoretical Computer Science**

2008 | journal-article

**Iterator types**

2007 | journal-article

**Linear recursive functions**

2007 | journal-article

**Sequence disunification and its application in collaborative schema construction**

2007 | journal-article

**The Power of Closed Reduction Strategies**

**Electronic Notes in Theoretical Computer Science**

2007 | journal-article

**Type-based static and dynamic website verification**

**Second International Conference on Internet and Web Applications and Services, ICIW'07**

2007 | journal-article

**Using intersection types for cost-analysis of higher-order polymorphic functional programs**

2007 | journal-article

**XCentric: A Logic-Programming Language for XML Processing**

**PLAN-X 2007, Programming Language Technologies for XML, An ACM SIGPLAN Workshop colocated with POPL 2007, Nice, France, January 20, 2007**

2007 | conference-paper

**XCentric: Logic programming for XML processing**

**International Conference on Information and Knowledge Management, Proceedings**

2007 | journal-article

**The power of linear functions**

2006 | journal-article

**Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs**

**Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers**

2006 | conference-paper

**VeriFLog: A constraint logic programming approach to verification of website content**

2006 | journal-article

**Weak linearization of the lambda calculus**

**Theoretical Computer Science**

2005 | journal-article

**CLP (Flex): Constraint logic programming applied to XML processing**

2004 | journal-article

**Linearization by program transformation**

2004 | journal-article

**Linearization of the lambda-calculus and its relation with intersection type systems**

**Journal of Functional Programming**

2004 | journal-article

**Type-based XML processing in logic programming**

2003 | journal-article

**On the Relation between Rank 2 Intersection Types and Simple Types**

**AGP 2002: Proceedings of the Joint Conference on Declarative Programming, APPIA-GULP-PRODE, Madrid, Spain, September 16-18, 2002.**

2002 | conference-paper

**Type inference using constraint handling rules**

**Electronic Notes in Theoretical Computer Science**

2002 | journal-article