arXiv subjects

Ugo de' Liguoro

Publications and source records attributed to Ugo de' Liguoro.

4 recordsLinked to original sources

arXiv2026

An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)

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 can be typed in this system, we define the Global Trace Condition (GTC), adapting the concept from Brotherston and Simpson's Cyclic Proofs, and show that any infinite reduction of a well-typed term satisfying the GTC is strongly convergent. As a corollary, we obtain the proof that any closed term of type Nat reduces to some numeral through any reduction by levels. We argue that the Church-Rosser in the limit holds for our calculus and, when restricted to regular terms, the calculus defines exactly the total functions defined in Das's Cyclic System T (an infinitary version of System T without $λ$), and hence in Goedel's System T.

cs.LO↗

arXiv2014

Loosening the notions of compliance and sub-behaviour in client/server systems

In the context of "session behaviors" for client/server systems, we propose a weakening of the compliance and sub-behaviour relations where the bias toward the client (whose "requests" must be satisfied) is pushed further with respect to the usual definitions, by admitting that "not needed" output actions from the server side can be "skipped" by the client. Both compliance and sub-behaviour relations resulting from this weakening remain decidable, though the proof of the duals-as-minima property for servers, on which the decidability of the sub-behaviour relation relies, requires a tighter analysis of client/server interactions.

cs.LO↗

arXiv2014

Compliance for reversible client/server interactions

In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via a LTS, and define a natural notion of checkpoint compliance. We then obtain a co-inductive characterisation of such compliance relation, and an axiomatic presentation that is proved to be sound and complete. As a byproduct we get a decision procedure for the new compliance, being the axiomatic system algorithmic.

cs.LO↗

arXiv2013

Non-monotonic Pre-fixed Points and Learning

We consider the problem of finding pre-fixed points of interactive realizers over arbitrary knowledge spaces, obtaining a relative recursive procedure. Knowledge spaces and interactive realizers are an abstract setting to represent learning processes, that can interpret non-constructive proofs. Atomic pieces of information of a knowledge space are stratified into levels, and evaluated into truth values depending on knowledge states. Realizers are then used to define operators that extend a given state by adding and possibly removing atoms: in a learning process states of knowledge change nonmonotonically. Existence of a pre-fixed point of a realizer is equivalent to the termination of the learning process with some state of knowledge which is free of patent contradictions and such that there is nothing to add. In this paper we generalize our previous results in the case of level 2 knowledge spaces and deterministic operators to the case of omega-level knowledge spaces and of non-deterministic operators.

cs.LO↗