BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Gianluca Curzi

Gianluca Curzi contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer Science

Trust snapshot

Quick read

Trust 17 - UnverifiedVerification L1Unclaimed author
4works
0followers
1topics
2close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

4 published item(s)

preprint2021arXiv

Linear Additives

We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: typable terms of LAM enjoy linear strong normalization. Moreover, a mildly weakened version of cut-elimination for this system is proven which takes a cubic number of steps. Finally, we define a sound translation from proofs of LAM into linear lambda terms of IMLL2, and we study its complexity.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A type-assignment of linear erasure and duplication

We introduce $\mathsf{LEM}$, a type-assignment system for the linear $ λ$-calculus that extends second-order $\mathsf{IMLL}_2$, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. $\mathsf{LEM}$ enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of $\mathsf{LEM}$ into $\mathsf{IMLL}_2$ exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. $\mathsf{LEM}$ allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, by contraction, and disposing garbage, by weakening. It can also represent natural numbers with terms very close to standard Church numerals which, moreover, apply to Hereditarily Finite Permutations, i.e. a group structure that exists inside the linear $ λ$-calculus.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Probabilistic Soft Type Assignment

We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Soft Linear Logic. PSTA is a type assignment for an extension of Simpson's Linear Lambda Calculus and its surface reduction, where Linear additives express random choice. Linear additives are weaker than the usual ones; they allow for duplications harmlessly affecting the computational cost of normalization. PSTA is sound and complete w.r.t. probabilistic polynomial time functions and characterizes the probabilistic complexity classes PP and BPP, the latter slightly less implicitly than PP.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

The Benefit of Being Non-Lazy in Probabilistic λ-calculus

We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specific operational semantics. This notion has been studied with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven to be fully abstract with respect to the contextual equivalence in cbv but not in lazy cbn. We overcome this issue of cbn by relaxing the laziness constraint: we prove that PAB is fully abstract with respect to the standard head reduction contextual equivalence. Our proof is based on the Leventis Separation Theorem, using probabilistic Nakajima trees as a tree-like representation of the contextual equivalence classes. Finally, we prove also that the inequality full abstraction fails, showing that the probabilistic applicative similarity is strictly contained in the contextual preorder.

0 citations0 reviewsNo code linkedOpen access