A nonstandard standardization theorem

DOI10.1145/2535838.2535886MaRDI QIDQ5408457zbMATH OpenOpenAlexFDO

Authors Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2535838.2535886

zbMATH Keywords

explicit substitutionslambda-calculusproof-netsresidualsstandardization

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Recommendations

• An abstract factorization theorem for explicit substitutions
• Standardization theorem revisited
• Proof nets and the linear substitution calculus
• scientific article; zbMATH DE number 7204428
• Term Rewriting and Applications

Cited in

(37)

• Projections for infinitary rewriting
• The spirit of node replication
• (In)efficiency and reasonable cost models
• On the value of variables
• Projections for infinitary rewriting (extended version)
• Classical by-need
• The useful MAM, a reasonable implementation of the strong -calculus
• Standardization theorem revisited
• Discrete normalization and standardization in deterministic residual structures
• Unification for -calculi without propagation rules
• A nonstandard Riemann existence theorem
• A resource aware semantics for a focused intuitionistic calculus
• scientific article; zbMATH DE number 7456059 (Why is no real title available?)
• The Negligible and Yet Subtle Cost of Pattern Matching
• A Fresh Look at the λ-Calculus
• scientific article; zbMATH DE number 7204428 (Why is no real title available?)
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• An abstract factorization theorem for explicit substitutions
• Tight typings and split bounds, fully developed
• Non-idempotent types for classical calculi in natural deduction style
• scientific article; zbMATH DE number 232909 (Why is no real title available?)
• A definable nonstandard enlargement
• Focused linear logic and the \(\lambda\)-calculus
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Node Replication: Theory And Practice
• Canonicity of proofs in constructive modal logic
• A strong bisimulation for a classical term calculus
• Exponentials as substitutions and the cost of cut elimination in linear logic
• On abstract normalisation beyond neededness
• Coherence by normalization for linear multicategorical structures
• IMELL cut elimination with linear overhead
• Mirroring call-by-need, or values acting silly
• Meaningfulness and genericity in a subsuming framework (invited talk)
• Sharing and linear logic with restricted access
• The benefits of diligence
• Mirroring call-by-need, or values acting silly
• Barendregt's theory of the -calculus, refreshed and formalized

This page was built for publication: A nonstandard standardization theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408457)