Zobrazeno 1 - 10
of 276
pro vyhledávání: '"Gavazzo P"'
We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, b
Externí odkaz:
http://arxiv.org/abs/2401.12744
Autor:
Gavazzo, Francesco
Moving from the mathematical theory of (abstract) syntax, we develop a general relational theory of symbolic manipulation parametric with respect to, and accounting for, general notions of syntax. We model syntax relying on categorical notions, such
Externí odkaz:
http://arxiv.org/abs/2305.01772
Autor:
Dagnino, Francesco, Gavazzo, Francesco
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 2 (April 4, 2024) lmcs:11041
Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed a
Externí odkaz:
http://arxiv.org/abs/2303.03271
We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability,
Externí odkaz:
http://arxiv.org/abs/2211.06671
We study the nature of applicative bisimilarity in $\lambda$-calculi endowed with operators for sampling from continuous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with context
Externí odkaz:
http://arxiv.org/abs/2207.10590
Autor:
Gavazzo, Francesco, Di Florio, Cecilia
We introduce a general theory of quantitative and metric rewriting systems, namely systems with a rewriting relation enriched over quantales modelling abstract quantities. We develop theories of abstract and term-based systems, refining cornerstone r
Externí odkaz:
http://arxiv.org/abs/2206.13610
We study the algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices without implementing the underlying selection mechanism, and give a fe
Externí odkaz:
http://arxiv.org/abs/2203.15426
Autor:
Francesco Dagnino, Francesco Gavazzo
Publikováno v:
Logical Methods in Computer Science, Vol Volume 20, Issue 2 (2024)
Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed a
Externí odkaz:
https://doaj.org/article/66a7ca6414fc4c2587804f833744143b
Autor:
Lago, Ugo Dal, Gavazzo, Francesco
We investigate program equivalence for linear higher-order(sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear $\lambda$-calculus with ex
Externí odkaz:
http://arxiv.org/abs/2106.12849
Autor:
Lago, Ugo Dal, Gavazzo, Francesco
Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for modal and coeffectful languages, however, is considera
Externí odkaz:
http://arxiv.org/abs/2103.03871