scientific article; zbMATH DE number 3400430
From MaRDI portal
Publication:5667469
zbMath0253.68007MaRDI QIDQ5667469
No author found.
Publication date: 1972
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Combinatory logic and lambda calculus (03B40) Algorithms in computer science (68W99)
Related Items (only showing first 100 items - show all)
Explicit cyclic substitutions ⋮ Higher-order unification, polymorphism, and subsorts ⋮ Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels ⋮ Tuning as convex optimisation: a polynomial tuner for multi-parametric combinatorial samplers ⋮ Inductively defined types in the Calculus of Constructions ⋮ Monads, indexes and transformations ⋮ Unnamed Item ⋮ Trakhtenbrot’s Theorem in Coq ⋮ Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Explicit substitutions with de bruijn's levels ⋮ Combinatory reduction systems with explicit substitution that preserve strong normalisation ⋮ Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ Programming and Proving with Classical Types ⋮ On the enumeration of closures and environments with an application to random generation ⋮ The Role of Indirections in Lazy Natural Semantics ⋮ Binding in Nominal Equational Logic ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ Non-linearity as the Metric Completion of Linearity ⋮ Term-Generic Logic ⋮ Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ Getting There and Back Again ⋮ Extensional higher-order paramodulation in Leo-III ⋮ An extension of system F with subtyping ⋮ Interactive and automated proofs for graph transformations ⋮ Mechanized Verification of CPS Transformations ⋮ Why Would You Trust B? ⋮ Finitary type theories with and without contexts ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Constraint handling rules with binders, patterns and generic quantification ⋮ Closure under alpha-conversion ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ A step towards absolute versions of metamathematical results ⋮ Variable binding and substitution for (nameless) dummies ⋮ The formal verification of the ctm approach to forcing ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Material dialogues for first-order logic in constructive type theory ⋮ Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers ⋮ Program equivalence in an untyped, call-by-value functional language with uncurried functions ⋮ Term-Graph Rewriting Via Explicit Paths ⋮ Counting and generating terms in the binary lambda calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Psi-calculi in Isabelle ⋮ Psi-calculi in Isabelle ⋮ Unnamed Item ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ A call-by-name lambda-calculus machine ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Context-relative syntactic categories and the formalization of mathematical text ⋮ On the expressiveness of internal mobility in name-passing calculi ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions ⋮ New Developments in Environment Machines ⋮ Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic ⋮ Explicit Substitutions à la de Bruijn ⋮ A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi ⋮ A Mechanized Model of the Theory of Objects ⋮ Abstract λ-Calculus Machines ⋮ Unnamed Item ⋮ Eigenvariables, bracketing and the decidability of positive minimal predicate logic ⋮ Unnamed Item ⋮ Innocent game models of untyped \(\lambda\)-calculus ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ On the proof theory of Coquand's calculus of constructions ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Type Theory Should Eat Itself ⋮ Rocket-Fast Proof Checking for SMT Solvers ⋮ Superposition with lambdas ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Unnamed Item ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Syntax for Free: Representing Syntax with Binding Using Parametricity ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations ⋮ The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Modeling and Verifying Graph Transformations in Proof Assistants ⋮ A Name Abstraction Functor for Named Sets ⋮ The practice of logical frameworks ⋮ Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ Eta-conversion for the languages of explicit substitutions ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation ⋮ The higher-order prover \textsc{Leo}-II ⋮ Third order matching is decidable ⋮ Nominal logic, a first order theory of names and binding ⋮ A general mathematics of names
Uses Software
This page was built for publication:
