Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
2 results

Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

Giulio Guerrieri ; Luca Paolini ; Simona Ronchi Della Rocca.
We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characterizations of many semantic properties. We prove that&nbsp;[&hellip;]
Published on December 22, 2017
Volume 13, Issue 4

Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

Giulio Guerrieri ; Luc Pellissier ; Lorenzo Tortora de Falco.
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion&nbsp;[&hellip;]
Published on April 22, 2022
Volume 18, Issue 2
  • < Previous
  • 1
  • Next >