3 papers
cs.LO2026
An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)
Stefano Berardi, Ugo de' Liguoro, Daisuke Kimura +1
We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Goedel's system T. For terms that ca…
cs.LO2026
Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday
Thorsten Altenkirch, Franco Barbanera, Ferruccio Damiani +1
Proof Theory and Type Theory are two branches of mathematical logic and theoretical computer science that explore the structure of mathematical proofs and the foundations of comput…
cs.LO2025
Intersection Types for a Computational Lambda-Calculus with Global State
Ugo de'Liguoro, Riccardo Treglia
We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to mod…