Search

• < Previous
• 1
• Next >

---

Proof-Relevant Logical Relations for Name Generation

Nick Benton ; Martin Hofmann ; Vivek Nigam.

Pitts and Stark's $\nu$-calculus is a paradigmatic total language for studying the problem of contextual equivalence in higher-order languages with name generation. Models for the $\nu$-calculus that validate basic equivalences concerning names may be constructed using functor categories or nominal&nbsp;[&hellip;]

---

Bounded Linear Logic, Revisited

Ugo Dal Lago ; Martin Hofmann.

We present QBAL, an extension of Girard, Scedrov and Scott's bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded linear logic considerably more flexible, while preserving soundness and completeness for&nbsp;[&hellip;]

---