scientific article; zbMATH DE number 5318491
From MaRDI portal
Publication:3522248
Recommendations
- scientific article; zbMATH DE number 3993540
- scientific article; zbMATH DE number 4002064
- The lambda calculus. Its syntax and semantics. Rev. ed.
- scientific article; zbMATH DE number 3875232
- On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
- scientific article; zbMATH DE number 2242116
- scientific article; zbMATH DE number 32501
- scientific article; zbMATH DE number 5852776
- scientific article; zbMATH DE number 4024773
Cited in
(86)- A solution to Curry and Hindley's problem on combinatory strong reduction
- Lambda terms definable as combinators
- The Church-Rosser theorem and quantitative analysis of witnesses
- The broadest necessity
- A formal system of reduction paths for parallel reduction
- A simplified proof of the Church-Rosser theorem
- A theory of necessities
- A Knuth-Bendix-like ordering for orienting combinator equations
- A combinator-based superposition calculus for higher-order logic
- Barendregt's problem \#26 and combinatory strong reduction
- Combinatory logic with polymorphic types
- The IO and OI hierarchies revisited
- Strong reduction of combinatory calculus with streams
- Structure by proxy, with an application to grounding
- Towards a homotopy domain theory
- Bounded combinatory logic and lower complexity
- Book review of: H. Barendregt et al., Lambda calculus with types
- A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
- Combinatory logic. Pure, applied and typed
- scientific article; zbMATH DE number 2185659 (Why is no real title available?)
- scientific article; zbMATH DE number 5852776 (Why is no real title available?)
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
- scientific article; zbMATH DE number 993359 (Why is no real title available?)
- A Short Introduction to Implicit Computational Complexity
- Verificationism and Classical Realizability
- Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey
- Bridging Curry and Church's typing style
- Bunder's paradox
- scientific article; zbMATH DE number 4147470 (Why is no real title available?)
- A Nominal Axiomatization of the Lambda Calculus
- An Introduction to the Lambda Calculus
- Unifying Math Ontologies: A Tale of Two Standards
- A decidable theory of type assignment
- scientific article; zbMATH DE number 4002064 (Why is no real title available?)
- scientific article; zbMATH DE number 4024773 (Why is no real title available?)
- scientific article; zbMATH DE number 192881 (Why is no real title available?)
- Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic
- scientific article; zbMATH DE number 1984512 (Why is no real title available?)
- Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 783760 (Why is no real title available?)
- scientific article; zbMATH DE number 919545 (Why is no real title available?)
- scientific article; zbMATH DE number 6148924 (Why is no real title available?)
- Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms
- Models of the lambda calculus: an introduction
- The search for a reduction in combinatory logic equivalent to -reduction. II.
- The Scott model of PCF in univalent type theory
- The combinator M and the Mockingbird lattice
- Normalization by Evaluation for Typed Weak lambda-Reduction
- The functional interpretation of direct computations
- Constructibility and Geometry
- Logic of intuitionistic interactive proofs (formal theory of perfect knowledge transfer)
- Imaginary groups: lazy monoids and reversible computation
- Clocks for Functional Programs
- scientific article; zbMATH DE number 2242116 (Why is no real title available?)
- Lower end of the linial-post spectrum
- Algebraic and Logical Operations on Operators One Application to Semantic Computation
- From semantics to types: the case of the imperative \(\lambda\)-calculus
- Mockingbird lattices
- A Formal Proof of the Strong Normalization Theorem for System T in Agda
- A (machine-oriented) logic based on pattern matching
- Core Type Theory
- A century since \textit{Principia}'s substitution bedazzled Haskell Curry. In honour of Jonathan Seldin's 80th anniversary
- The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction
- A lambda calculus satellite
- Logical predicates in higher-order mathematical operational semantics
- Puzzles of existential generalisation from type-theoretic perspective
- The internal operads of combinatory algebras
- Combinators as presheaves
- Factorize factorization
- Computational expressivity of (circular) proofs with fixed points
- Categorification of characteristic structures
- Proof-theoretic investigation of -reduction in the simply typed -calculus
- Computational paths -- a weak groupoid
- Two cases of deduction with non-referring descriptions
- A weakly initial algebra for higher-order abstract syntax in Cedille
- The ineffability of God – a logical approach
- Braids, twists, trace and duality in combinatory algebras
- Bialgebraic reasoning on higher-order program equivalence
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- The K_ homotopy -model
- Extending computational trinitarianism
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Reduction rules for intuitionistic -calculus
- Lambda calculus with patterns
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3522248)
