Parallel reductions in \(\lambda\)-calculus
From MaRDI portal
Publication:5917605
DOI10.1006/inco.1995.1057zbMath0827.68060OpenAlexW2018181305MaRDI QIDQ5917605
Publication date: 13 December 1995
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1995.1057
Related Items
Formal metatheory of the lambda calculus using Stoughton's substitution, Confluence of orthogonal term rewriting systems in the prototype verification system, Upper bounds for standardizations and an application, The Church-Rosser theorem and quantitative analysis of witnesses, Unnamed Item, I Got Plenty o’ Nuttin’, More Church-Rosser proofs (in Isabelle/HOL), A lambda-calculus for dynamic binding, Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters, Amortized Complexity Verified, A domain-theoretic semantics of lax generic functions., Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, A deterministic rewrite system for the probabilistic λ-calculus, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Typed operational semantics for higher-order subtyping., Decomposing probabilistic lambda calculi, Unnamed Item, Reasoning about multi-stage programs, The untyped computational \(\lambda \)-calculus and its intersection type discipline, Unnamed Item, Head reduction and normalization in a call-by-value lambda-calculus, Nominal techniques in Isabelle/HOL, Factorization in call-by-name and call-by-value calculi via linear logic, A formalized general theory of syntax with bindings: extended version, A formal system of reduction paths for parallel reduction, Compositional Z: confluence proofs for permutative conversion, Proof Pearl: Abella Formalization of λ-Calculus Cube Property, From Search to Computation: Redundancy Criteria and Simplification at Work, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Strong normalization of classical natural deduction with disjunctions, Tactics and Parameters, Non-strictly positive fixed points for classical natural deduction, A simplified proof of the Church-Rosser theorem, Unnamed Item, Monotone (co)inductive types and positive fixed-point types, On the confluence of lambda-calculus with conditional rewriting, A proof of the leftmost reduction theorem for \(\lambda\beta\eta\)-calculus, A typed context calculus, Unnamed Item, Perpetual reductions in \(\lambda\)-calculus, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), The lambda-context calculus (extended version), Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory, Descendants and origins in term rewriting., Conservation and uniform normalization in lambda calculi with erasing reductions, Term Collections in λ and ρ-calculi, Church-Rosser property of a simple reduction for full first-order classical natural deduction, 1999–2000 Winter Meeting of the Association for Symbolic Logic, Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention, Distributive ρ-calculus, Abstract abstract reduction
