scientific article; zbMATH DE number 482822

Publication date: 15 December 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

models type systems combinatory logic pure lambda-calculus

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Semantics in the theory of computing (68Q55) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

A general storage theorem for integers in call-by-name $\lambda$- calculus, Semantic analysis of normalisation by evaluation for typed lambda calculus, Getting results from programs extracted from classical proofs, Graph easy sets of mute lambda terms, Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic, Intersection types for explicit substitutions, Fresh logic: Proof-theory and semantics for FM and nominal techniques, Strong normalization for non-structural subtyping via saturated sets, Unnamed Item, Strong normalization from weak normalization in typed $\lambda$-calculi, A resource aware semantics for a focused intuitionistic calculus, A semantical storage operator theorem for all types, Unnamed Item, Unnamed Item, Typing total recursive functions in Coq, A relational semantics for parallelism and non-determinism in a functional setting, Computational isomorphisms in classical logic, System ST toward a type system for extraction and proofs of programs, A formalised first-order confluence proof for the $\lambda$-calculus using one-sorted variable names., Classical realizability and arithmetical formulæ, Non-idempotent intersection types in logical form, Böhm theorem and Böhm trees for the $\varLambda \mu$-calculus, Completeness and partial soundness results for intersection and union typing for $\overline{\lambda}\mu\tilde{\mu}$, Tight typings and split bounds, fully developed, A binary modal logic for the intersection types of lambda-calculus., Implicative algebras: a new foundation for realizability and forcing, Behavioural inverse limit $\lambda$-models, Validating Brouwer's continuity principle for numbers using named exceptions, The graphical Krivine machine, A call-by-name lambda-calculus machine, Controlling Program Extraction in Light Logics, A Filter Model for the λμ-Calculus, Strong normalization through intersection types and memory, Decidability of all minimal models, On automating the extraction of programs from proofs using product types, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, Forcing in stable models of untyped $\lambda$-calculus, A $\kappa$-denotational semantics for map theory in ZFC+SI, Unnamed Item, Some Remarks on Type Systems for Course-of-value Recursion, An ordinal measure based procedure for termination of functions, Completeness, minimal logic and programs extraction, Non-strictly positive fixed points for classical natural deduction, A Relational Model of a Parallel and Non-deterministic λ-Calculus, On the construction of stable models of untyped $\lambda$-calculus, Specifying Imperative ML-Like Programs Using Dynamic Logic, Unnamed Item, Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $$\lambda $$ λ -terms, Reasoning About Call-by-need by Means of Types, On the Values of Reducibility Candidates, A Fresh Look at the λ-Calculus, Focalisation and Classical Realisability, Strong normalization of $\mathsf{ML}^{\mathsf F}$ via a calculus of coercions, Building continuous webbed models for system F, Perpetual reductions in $\lambda$-calculus, Dedekind completion as a method for constructing new Scott domains, From computation to foundations via functions and application: The $\lambda$-calculus and its webbed models, (In)efficiency and reasonable cost models, Term-generic logic, Higher order unification via explicit substitutions, Descendants and origins in term rewriting.