Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem

No abstract is available for this paper.

• Publication year

  1972

• Venue

  Studies in logic and the foundations of mathematics

• Publication date

  Unknown publication date

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1016/S0049-237X(08)70216-7
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The mathematical language AUTOMATH, its usage, and some of its extensions

  1970cited by this paper
• The calculi of lambda-conversion

  1941cited by this paper

• Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-\v{C}ubri\'c Interpolation

  2026cites this paper
• Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

  2026cites this paper
• An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus

  2026influential citation
• Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem

  2026cites this paper
• Towards a Higher-Order Bialgebraic Denotational Semantics

  2026cites this paper
• Normalisation for First-Class Universe Levels

  2026cites this paper
• Implementing Dependent Type Theory Inhabitation and Unification

  2026cites this paper
• A Calculus of Inheritance

  2026cites this paper
• Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs

  2025cites this paper
• A Logic For Fresh Labelled Transition Systems

  2025cites this paper
• Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments

  2025cites this paper
• On the Challenges of Quantum Circuit Encoding Using Deep and Reinforcement Learning

  2025cites this paper
• Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi

  2025cites this paper
• Algebraic Stepper for Simple Modules

  2025cites this paper
• The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem

  2025cites this paper
• QuickSub: Efficient Iso-Recursive Subtyping

  2025cites this paper
• Rebound: Efficient, Expressive, and Well-Scoped Binding

  2025cites this paper
• Logics of Statements in Context—First-Order Logic Files

  2025cites this paper
• Type Theory with Single Substitutions

  2025cites this paper
• Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language

  2025cites this paper
• Zero-Overhead Lexical Effect Handlers

  2025cites this paper
• On a Dependently Typed Encoding of Matching Logic

  2025cites this paper
• D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation

  2025cites this paper
• Modular abstract syntax trees (MAST): substitution tensors with second-class sorts

  2025cites this paper
• Type-Safe Compilation of Dynamic Inheritance via Merging

  2025cites this paper
• Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

  2025cites this paper
• E-Graphs With Bindings

  2025cites this paper
• FuseFlow: A Fusion-Centric Compilation Framework for Sparse Deep Learning on Streaming Dataflow

  2025cites this paper
• Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings

  2025cites this paper
• An Isabelle/HOL Framework for Synthetic Completeness Proofs

  2025cites this paper
• Learning Automata with Name Allocation

  2025cites this paper
• POLYMORPHISM AND MINIMAL TYPES WITHOUT DEPENDENT PRODUCTS

  2025cites this paper
• A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums

  2025cites this paper
• Canonical for Automated Theorem Proving in Lean

  2025cites this paper
• AdapTT: Functoriality for Dependent Type Casts

  2025cites this paper
• A Mechanized Formalization of an FRP Language with Effects

  2025cites this paper
• Naturality for higher-dimensional path types

  2025cites this paper
• Term Orders for Optimistic Lambda-Superposition

  2025cites this paper
• Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang

  2025cites this paper
• Structured Monads for Generic First-Order Syntax Metatheory

  2025cites this paper
• Certified Compilation based on Gödel Numbers

  2025cites this paper
• Substitution Without Copy and Paste

  2025cites this paper
• A simple formalization of alpha-equivalence

  2025cites this paper
• LISA - A Modern Proof System

  2025cites this paper
• A Sound and Complete Projection for Global Types

  2025cites this paper
• Generating Function Names to Improve Comprehension of Synthesized Programs

  2024cites this paper
• Pantograph: A Fluid and Typed Structure Editor

  2024cites this paper
• Abstractions for Multi-Sorted Substitutions

  2024cites this paper
• Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions

  2024cites this paper
• A Logical Approach to Type Soundness

  2024cites this paper
• Property-Based Testing by Elaborating Proof Outlines

  2024cites this paper
• WebPie: A Tiny Slice of Dependent Typing

  2024cites this paper
• Compiling Probabilistic Programs for Variable Elimination with Information Flow

  2024cites this paper
• Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)

  2024cites this paper
• Polymorphic higher-order context-free session types

  2024cites this paper
• Free Foil: Generating Efficient and Scope-Safe Abstract Syntax

  2024cites this paper
• On the Expressive Power of Languages for Static Variability

  2024cites this paper
• A Case for First-Class Environments

  2024cites this paper
• Modal μ-Calculus for Free in Agda

  2024cites this paper
• Embedding Differential Dynamic Logic in PVS

  2024cites this paper
• Guided Equality Saturation

  2024cites this paper
• Context-Free Binding Grammars

  2024cites this paper
• Generative Explanations for Program Synthesizers

  2024cites this paper
• Building a cognitive system based on process interaction

  2024cites this paper
• Learning Structure-Aware Representations of Dependent Types

  2024cites this paper
• Scoped and Typed Staging by Evaluation

  2023cites this paper
• The Sequence Notation: Catching Complex Meanings in Simple Graphs

  2023cites this paper
• Multi-Stage Vertex-Centric Programming for Agent-Based Simulations

  2023cites this paper
• Detecting Interpreter Bugs via Filling Function Calls in Skeletal Program Enumeration

  2023cites this paper
• System $F^\mu_\omega$ with Context-free Session Types

  2023cites this paper
• Type system for λσ-calculus with all de Bruijn indices

  2023cites this paper
• Builtin Types viewed as Inductive Families

  2023cites this paper
• HOπ in Coq

  2023cites this paper
• Grisette: Symbolic Compilation as a Functional Programming Library

  2023cites this paper
• HOπ in Coq

  2023cites this paper
• Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties

  2023cites this paper
• Bachelorthesis Computer Science Implementing Abstract Machines in SQL

  2023cites this paper
• Latent Idiom Recognition for a Minimalist Functional Array Language Using Equality Saturation

  2023cites this paper
• No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System

  2023cites this paper
• Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

  2023cites this paper
• Syntax Monads for the Working Formal Metatheorist

  2023influential citation
• Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure

  2023cites this paper
• Transplanting of Environments between Closures in the lambda calculus

  2023cites this paper
• Material dialogues for first-order logic in constructive type theory: extended version

  2023cites this paper
• Towards a Neural Lambda Calculus: Neurosymbolic AI Applied to the Foundations of Functional Programming

  2023cites this paper
• Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq

  2023cites this paper
• Extensible Metatheory Mechanization via Family Polymorphism

  2023cites this paper
• α-Avoidance

  2023influential citation
• Locally Nameless Sets

  2023cites this paper
• Verified Encodings for SAT Solvers

  2023cites this paper
• Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL

  2023cites this paper
• Renamingless Capture-Avoiding Substitution for Definitional Interpreters

  2023cites this paper
• Ideograph: A Language for Expressing and Manipulating Structured Data

  2023cites this paper
• HOTGP - Higher-Order Typed Genetic Programming

  2023cites this paper
• A Formal Proof of the Strong Normalization Theorem for System T in Agda

  2023cites this paper
• Towards Modular Compilation Using Higher-Order Effects

  2023cites this paper
• Logic of Differentiable Logics: Towards a Uniform Semantics of DL

  2023cites this paper
• A Formalisation of Core Erlang, a Concurrent Actor Language

  2023cites this paper
• Program equivalence in an untyped, call-by-value functional language with uncurried functions

  2023cites this paper
• Triemaps that match

  2023cites this paper