scientific article; zbMATH DE number 3280068

Cited in

(only showing first 100 items - show all)

A construction of one-point bases in extended lambda calculi
Linear logic by levels and bounded time complexity
Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
A characterization of F-complete type assignments
Word operation definable in the typed -calculus
One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus
Substitution revisited
The calculus of constructions
Principal type scheme and unification for intersection type discipline
Conditional rewrite rules: Confluence and termination
BCK-combinators and linear \(\lambda\)-terms have types
On pseudo-c normal form in combinatory logic
Indexings of subrecursive classes
From types to sets
Invertible terms in the lambda calculus
An efficient interpreter for the lambda-calculus
The IO- and OI-hierarchies
Pre-recursive categories
On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
Conditional rewriting logic as a unified model of concurrency
Complete restrictions of the intersection type discipline
Intersection types for combinatory logic
Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
How to decide the lark
Call-by-name, call-by-value and the \(\lambda\)-calculus
An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
Quantifier-complete categories
Functionals computable in series and in parallel
Characterization of normal forms possessing inverse in the - --calculus
A global representation of the recursive functions in the \(\lambda\)- calculus
A discrimination algorithm inside --calculus
Intuitionistic propositional logic is polynomial-space complete
Abstraction problems in combinatory logic: A compositive approach
From constructivism to computer science
A finite equational axiomatization of the functional algebras for the lambda calculus
Perpetual reductions in -calculus
Some examples of non-existent combinators
Combining type disciplines
The connection between an event structure semantics and an operational semantics for TCSP
Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends
Lambda terms definable as combinators
Intersection type assignment systems
Normalization results for typeable rewrite systems
Strong normalization from weak normalization in typed \(\lambda\)-calculi
Full abstraction and recursion
Developing developments
On the strong normalisation of intuitionistic natural deduction with permutation-conversions
A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
A binary modal logic for the intersection types of lambda-calculus.
On the algebraic models of lambda calculus
Intensional computation with higher-order functions
On the representation of semigroups and other congruences in the lambda calculus
Projections for infinitary rewriting
An algebraic framework for minimum spanning tree problems
Typing and computational properties of lambda expressions
A set of combinators for abstraction in linear space
Towards a computation system based on set theory
Sequential evaluation strategies for parallel-or and related reduction systems
The completeness theorem for typing lambda-terms
Efficient multi-variate abstraction using an array representation for combinators.
Descendants and origins in term rewriting.
Variants of the basic calculus of constructions
On the \(\lambda Y\) calculus
Parametric parameter passing \(\lambda\)-calculus
The Girard-Reynolds isomorphism
On completeness and cocompleteness in and around small categories
On randomised strategies in the -calculus
From distributed coordination to field calculus and aggregate computing
Partial combinatory algebra and generalized numberings
A type-assignment of linear erasure and duplication
Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
(In)efficiency and reasonable cost models
Formal metatheory of the lambda calculus using Stoughton's substitution
Higher-order unification via combinators
Projections for infinitary rewriting (extended version)
Nominal Lawvere theories: a category theoretic account of equational theories with names
A higher-order calculus and theory abstraction
The mechanisation of Barendregt-style equational proofs (the residual perspective)
Strongly normalising cut-elimination with strict intersection types
Predicate calculus of arbitrarily high finite order
λ-definable functionals andβη conversion
Proposal for a natural formalization of functional programming concepts
European meeting of the Association for Symbolic Logic, Mons, Belgium, 1978
scientific article; zbMATH DE number 3672268 (Why is no real title available?)
scientific article; zbMATH DE number 3741397 (Why is no real title available?)
Completeness, invariance and λ-definability
Stratification and cut-elimination
Alpha equivalence equalities
Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
Realizability algebras III: some examples
Krivine machines and higher-order schemes
Towards lambda calculus order-incompleteness
Automath and Pure Type Systems
Encoding the factorisation calculus
scientific article; zbMATH DE number 7453187 (Why is no real title available?)
Gate splitting in LOTOS specifications using abstract interpretation
The search for a reduction in combinatory logic equivalent to -reduction. II.
Representing model theory in a type-theoretical logical framework
Formal SOS-Proofs for the Lambda-Calculus
scientific article; zbMATH DE number 4195910 (Why is no real title available?)

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 Q5565113)