European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

June 5-6, 2025

The Workshop on Reasoning with Quantitative Types is a two day event, supported by the European Research Network on Formal Proofs. Intersection types were introduced near the end of the 1970s to overcome the limitations of Curry’s type assignment system and to provide a characterization of the strongly normalizing terms of the Lambda Calculus. The non-idempotent type discipline, introduced almost two decades later, was inspired by linear logic and has since been considered as an adequate model to reason about resources. This workshop aims at bringing together researchers who are currently developing theory and applications in this area, to foster their interaction and provide a forum for presenting new ideas and work in progress, as well as to enable newcomers to learn about current activities in this field.

Invited Speakers

  • Delia Kesner
  • Andrej Dudenhefner
  • Beniamino Accattoli

Call for contributed talks

  • Submission deadline: April 28, 2025
  • Author notification: May 4, 2025

The workshop is going to be an informal event and both original and previously submitted works will be considered. Contributed talks should be supported by a small abstract of 1 page. Please use the EasyChair style for formatting your submission (EasyChair Style Guidelines). Abstracts will not be peer-reviewed, but only those that are relevant and of good quality will be considered. Submit your abstracts as a PDF file via email to (sandra@fc.up.pt) before the submission deadline on April 28, 2025 (anywhere on Earth).

Venue

Department of Computer Science Faculty of Sciences - University of Porto Rua do Campo Alegre 1055, 4169-007 Porto, Portugal

Registration and Funding applications:

  • Application deadline: April 28, 2025
  • Notification: May 4, 2025
  • Extended application deadline: May 18,2025 (applications will be consider in order of arrival)

Participation at the WRQT 2025 is free, but registration is mandatory. To register, please use the registration/funding application form.

The EuroProofNet COST action can provide funding for a limited amount of participants. Before applying for funding see reimbursement rules.

Note that it is possible to arrive a few days before and leave a few days after the workshop but a maximum of 3.4 daily allowances will be reimbursed.

Please contact the organisers if you have any problem during the application for funding process, including reluctance to use google forms.

Program

The following is a tentative program (subject to change).

Day 1 - June 5, 2025

Time Session
09:00-09:30 Opening & Welcome
09:30-10:30 Invited talk - Delia Kesner: “An Introduction to Quantitative Types”
10:30-11:00 Coffee Tea Break
11:00-11:45 Giulio Guerrieri: “Relational semantics: from simple to non-idempotent intersection types and back”
11:45-12:30 Daniele Pautasso: “Typability in Simple Restrictions of Non-idempotent Intersection Types”
12:30-14:00 Lunch
14:30-15:30 Invited talk - Beniamino Accattoli: “Measuring Space via Multi Types”
15:30-16:00 Mário Florido: “Structural Rules and Algebraic Properties of Intersection Types”
16:00-16:30 Coffee Tea Break
16:30-17:15 Adrienne Lancelot: “Separating Terms by means of Multi Types, Coinductively”
17:15-18:00 Giulio Guerrieri: “Strong Call-by-Value and Multi Types”

Day 2 - June 6, 2025

Time Session
09:30-10:30 Tutorial - Andrej Dudenhefner: “Mechanization of Non-idempotent Intersection Types in the Coq Proof Assistant”
10:30-11:00 Coffee Tea Break
11:00-12:30 Tutorial - Andrej Dudenhefner: “Mechanization of Non-idempotent Intersection Types in the Coq Proof Assistant”
12:30-14:30 Lunch
14:30-15:30 Delia Kesner: “Quantitative Types for Call-by-Value”
15:30-16:00 Michał J. Gajda: “Dependent type system for Ultrafinitist Logic”
16:00-16:30 Coffee Tea Break
16:30 Closing

Organization