Deciding coproduct equality with focusing. Online draft, p.13, 2010. ,
Normalization by evaluation for lambda -2, FLOPS, p.13, 2004. ,
DOI : 10.1007/978-3-540-24754-8_19
URL : http://www.cs.nott.ac.uk/~txa/publ/flops04.pdf
Normalization by evaluation for typed lambda calculus with coproducts, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, 2001. ,
DOI : 10.1109/LICS.2001.932506
Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, 1992. ,
DOI : 10.1093/logcom/2.3.297
Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, POPL, p.13, 2004. ,
DOI : 10.1145/964001.964007
URL : https://hal.archives-ouvertes.fr/hal-00149561
Alcune proprieta delle forme normali nel k-calcolo, IAC Pubbl, vol.696119, issue.1, p.13, 1968. ,
Canonical Sequent Proofs via Multi-Focusing, IFIP TCS, 2007. ,
DOI : 10.1007/978-0-387-09680-3_26
URL : https://hal.archives-ouvertes.fr/hal-00527893
A logical characterization of forward and backward chaining in the inverse method, J. Autom. Reasoning, vol.40, issue.6, p.12, 2008. ,
A Systematic Approach to Canonicity in the Classical Sequent Calculus, CSL, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00772396
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL, p.12 ,
URL : https://hal.archives-ouvertes.fr/hal-01256092
Equality between functionals in the presence of coproducts, Information and Computation, vol.157, issue.2, p.12, 2000. ,
Lambda Definability with Sums via Grothendieck Logical Relations, TLCA, 1999. ,
DOI : 10.1007/3-540-48959-2_12
URL : http://www.cogs.susx.ac.uk/users/marcelo/papers/Types/glr.ps
Equality between functionals, Logic Colloquium, 1975. ,
DOI : 10.1007/BFb0064870
Beta-Eta Equality for Coproducts, TLCA, 1995. ,
DOI : 10.1007/bfb0014052
The exp-log normal form of types and canonical terms for lambda calculus with sums ,
Focusing and polarization in intuitionistic logic. CoRR, arxiv:0708.2252, 2007. ,
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231
Extensional Rewriting with Sums, TLCA, 2007. ,
DOI : 10.1007/978-3-540-73228-0_19
URL : http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf
Polarised Intermediate Representation of Lambda Calculus with Sums, 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, p.12, 2015. ,
DOI : 10.1109/LICS.2015.22
URL : https://hal.archives-ouvertes.fr/hal-01160579
Which types have a unique inhabitant? Focusing on pure program equivalence, 2016. ,
DOI : 10.1145/2784731.2784757
URL : https://hal.archives-ouvertes.fr/tel-01309712
Which simple types have a unique inhabitant, ICFP, 2015. ,
DOI : 10.1145/2784731.2784757
URL : https://hal.archives-ouvertes.fr/hal-01235596
Structural focalization. CoRR, arxiv:1109, 2011. ,
DOI : 10.1145/2629678
Categorical completeness results for the simply-typed lambda-calculus, TLCA, p.12, 1995. ,
DOI : 10.1007/BFb0014068
URL : http://www.dcs.ed.ac.uk/home/als/Research/completeness.ps.gz
Completeness, equivalence and lambda-definability, Journal of Symbolic Logic, vol.47, issue.1 1, 1982. ,
DOI : 10.2307/2273377
The Logical Basis of Evaluation Order and Pattern- Matching, p.12, 2009. ,
Polarity in proof theory and programming, 2013. URL http://noamz.org/talks/logpolpro.pdf. Lecture Notes for the Summer School on Linear Logic and Geometry of Interaction ,