Postdoctoral Researcher

Contract Calculi and Verifiable Agent Tools

Bocconi · REALMilan, ItalyFull time · Two years

Call upcoming

Connect contract semantics, compositional guarantees, and executable tool specifications.

Your role

You will develop formal foundations for agents that act, use resources and delegate authority under explicit commitments. This raises questions that extend beyond the verification of one implementation: how should contracts describe evolving interactions, what does it mean for commitments to compose, and which guarantees can survive changes in state or a transfer of responsibility to another agent? The position offers an opportunity to shape that scientific agenda.

You will develop an independent line of research connecting foundational theory and mechanized reasoning. The agenda spans dependent type theory, semantics, compositional verification, resource representations and their connections to executable systems. These themes offer substantial research directions for researchers focused on foundations or implementation. You will establish a focused contribution within this wider programme, working with a team whose expertise covers complementary parts of the agenda.

Within PC2, the research encompasses extensions to the contract calculus and methods for representing domains, resources and tool effects so that admissible actions can be characterised precisely. Questions include reasoning about contractual state, obligations and authority, preserving commitments through delegation, and connecting tool behaviour to the evidence needed before an action can proceed. The objective is reusable specification and verification methods connecting expressive domain models with tractable guarantees.

You will collaborate with systems and learning researchers to explore how these formal choices affect execution and proof generation. Research directions include compositional rules with mechanized guarantees, resource representations that simplify reasoning, and abstractions that transfer between domains. Filesystem access, messaging and operations such as payments provide contrasting domains for developing and evaluating these methods. As the work matures, there will be opportunities to help steward public specifications and formal libraries.

Your contribution to the field

Your contribution will strengthen the mathematical foundations of agents that act under contracts. The agenda connects new calculi, compositional rules, resource abstractions and mechanized results to emerging questions about autonomous action and delegation. By developing reusable specification and verification methods, you will establish an independent line of research with relevance beyond PC2 and help shape the formal interfaces on which other researchers and agent systems build.

An initial research or development direction

An example starting point is to investigate a question about contract composition or tool semantics through a precise model and a central theoretical or mechanized result, then examine its implications in a small executable case. Foundational analysis and reusable proof infrastructure provide complementary routes into this agenda.

Essential background

A PhD in computer science, mathematics or a closely related field; the required stage of completion and formal eligibility will be specified in the final call.
Research experience in formal methods and dependent type theory, through foundational work, formal specification, mechanization or verification research.
Ability to develop precise definitions and rigorous arguments, and communicate a research contribution clearly.
Interest in connecting formal foundations to agent interaction, resources or tool use. Complementary strengths in theory and practical formalization are valued.

Additional relevant experience

Compositional verification, programming language semantics, reasoning about resource constraints, protocol verification or automated reasoning.
Experience with Lean, Rocq/Coq, Agda or other proof assistant environments; no particular assistant is a universal entry requirement.
Reusable formal libraries, proof automation, verified interfaces or research software development.

Candidates with depth in a relevant area and an interest in connecting it to others are encouraged to apply. Evidence of your contribution can include research papers, formal developments, substantial software or a clear account of technical work that cannot be shared publicly.

Research environment and development

Your primary supervisor will be Alessandro Rudi. PC2 is a joint effort involving PRAXIS at AI4I, the REAL team at Bocconi and STAMP at Inria. The role requires close collaboration with the other participating groups, including opportunities for extended visiting periods at their laboratories, bringing your work into close contact with complementary expertise in machine learning, formal methods and systems.

The position is based in Milan, Italy. Remote working arrangements can be agreed when working from another laboratory in the PC2 collaboration. The timing and practical arrangements for research visits will be discussed with you and the participating hosts.

Computational resources. The joint programme is supported by AI4I's HPC infrastructure: approximately 150 NVIDIA GPUs (80 Blackwell B200 and 68 Hopper H200) and 5 PB of storage for agentic AI training, testing and validation. Access for collaborative projects will be arranged through the participating teams.

Application materials

Please prepare:

Your CV, including relevant research or technical experience.
A short statement of fit and interests, explaining what attracts you to the role, the experience you would bring and directions you would be interested in exploring. A full research proposal is not required.
One or two representative contributions, such as papers, formal developments or software. Briefly explain your own contribution. An account of work that cannot be shared publicly is welcome; a public repository is not required.

Submission instructions and the application deadline will be published here when the call is finalised.