Polarised Intermediate Representation of Lambda Calculus with Sums

Reference. Polarised Intermediate Representation of Lambda Calculus with Sums

Cite

Cite as @munchmaccagnoni-2015-polarised (helia, typst) · \cite{munchmaccagnoni-2015-polarised} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{munchmaccagnoni-2015-polarised, title={Polarised Intermediate Representation of Lambda Calculus with Sums}, url={http://dx.doi.org/10.1109/lics.2015.22}, DOI={10.1109/lics.2015.22}, booktitle={2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science}, publisher={IEEE}, author={Munch-Maccagnoni, Guillaume and Scherer, Gabriel}, year={2015}, month=July, pages={127–140} }

hayagriva YAML (typst)

yaml · 14 lines

munchmaccagnoni-2015-polarised:
  type: article
  title: Polarised Intermediate Representation of Lambda Calculus with Sums
  author:
  - Munch-Maccagnoni, Guillaume
  - Scherer, Gabriel
  date: 2015-07
  page-range: 127-140
  serial-number:
    doi: 10.1109/lics.2015.22
  parent:
    type: proceedings
    title: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
    publisher: IEEE

Download: munchmaccagnoni-2015-polarised.bib · munchmaccagnoni-2015-polarised.yml

Cited by (1)

A theory of effects and resources: adjunction models and polarised calculi curien-2016-aPOPL · 2016

DOI · pldb

Cites 69 works (8 here)

With notes (8)

Formulae-as-types for an involutive negation munchmaccagnoni-2014-formulaeLICS · 2014

DOI

Models of a Non-associative Composition munchmaccagnoni-2014-modelsFoSSaCS · 2014

DOI

The Duality of Computation under Focus curien-2010-theIFIP TCS · 2010

DOI · arXiv

Focalisation and Classical Realisability munchmaccagnoni-2009-focalisationCSL · 2009

DOI

On the unity of duality zeilberger-2008-onAPAL · 2008

DOI

Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalueSemantic Structures in Computation · 2003

DOI

Introduction to Higher-Order Categorical Logic lambek_scott_19861986

Web

Normalization by evaluation for typed lambda calculus with coproducts altenkirch_etal_ndLICS

Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as “normalization by evaluation”, and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.

DOI

External (61)

Multi-focusing on extensional rewriting with sums (2015)
A dissection of L (2014)
Structural Focalization (2014)
The Duality of Construction (2014)
A multi-focused proof system isomorphic to expansion proofs (2014)
Quantitative classical realizability (2014)
Proofs, Upside Down: A Functional Correspondence between Natural Deduction and the Sequent Calculus (2013)
Syntax and Models of a non-Associative Composition of Programs and Proofs (2013)
The Blind Spot: Lectures on Logic (2011)
Resource modalities in tensor logic (2010)
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi (2009)
Sequent calculi and abstract machines (2009)
Focusing and polarization in linear, intuitionistic, and classical logics (2009)
The logical basis of evaluation order and pattern-matching (2009)
A Rational Deconstruction of Landin's SECD Machine with the J Operator (2008)
Canonical Sequent Proofs via Multi-Focusing (2008)
Compiling with continuations, continued (2007)
Completing Herbelin’s Programme (2007)
Focusing and Polarization in Intuitionistic Logic (2007)
Extensional Rewriting with Sums (2007)
Le Point Aveugle, Cours de logique, Tome II: Vers l'imperfection (2007)
Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative (2006)
C'est maintenant qu'on calcule : au cœur de la dualité (2005)
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs (2005)
Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums (2004)
Call-by-value is dual to call-by-name (2003)
A functional correspondence between evaluators and abstract machines (2003)
Étude de la polarisation en logique (2002)
Locus Solum: From the Rules of Logic to the Logic of Rules (2001)
Control categories and duality: on the categorical semantics of the lambda-mu calculus (2001)
Defunctionalization at Work (2001)
Continuations Revisited (2000)
The duality of computation (2000)
Call-by-Push-Value: A Subsuming Paradigm (1999)
Classical logic, continuation semantics and abstract machines (1998)
Definitional Interpreters Revisited (1998)
A new deconstructive logic: linear logic (1997)
Categorical Structure of Continuation Passing Style (1997)
βη-Equality for coproducts (1995)
Lambda-calculus structure isomorphic to sequent calculus structure (1994)
Continuation Semantics or Expressing Implication by Negation (1993)
On the unity of logic (1993)
The discoveries of continuations (1993)
Some lambda calculi with categorical sums and products (1993)
Normal Forms and Cut-Free Proofs as Natural Transformations (1992)
Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction (1992)
Logic Programming with Focusing Proofs in Linear Logic (1992)
On the expressive power of programming languages (1991)
A new constructive logic: classic logic (1991)
Higher-order critical pairs (1991)
An algorithm for testing conversion in type theory (1991)
A note on inconsistencies caused by fixpoints in a cartesian closed category (1990)
Declarative Continuations and Categorical Duality (1989)
Continuation-Based Program Transformation Strategies (1980)
Continuations: A Mathematical Semantics for Handling Full Jumps (1974)
Definitional interpreters for higher-order programming languages (1972)
Diagonal arguments and cartesian closed categories (1969)
Recursive definition of syntax and semantics (1966)
Correspondence between ALGOL 60 and Church's Lambda-notation: part I (1965)
The Mechanical Evaluation of Expressions (1964)
Untersuchungen über das logische Schließen. I (1935)