The Bang Calculus and the Two Girard's Translations

April 15, 2019 · The Ethereal · 🏛 Linearity-TLLA@FLoC

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Giulio Guerrieri, Giulio Manzonetto arXiv ID 1904.06845 Category cs.LO: Logic in CS Cross-listed cs.DM, cs.PL Citations 31 Venue Linearity-TLLA@FLoC Last Checked 2 months ago
Abstract
We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both call-by-name and call-by-value lambda-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value lambda-calculi from a syntactic and a semantic viewpoint.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS