scientific article
From MaRDI portal
Publication:3204055
zbMath0716.68065MaRDI QIDQ3204055
Publication date: 1989
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Related Items
A theory of bisimulation for a fragment of concurrent ML with local names, Quantitative logics for equivalence of effectful programs, On reduction-based process semantics, Innovations in computational type theory using Nuprl, A two-valued logic for properties of strict functional programs allowing partial functions, Labelled reductions, runtime errors, and operational subsumption, Full abstraction and the Context Lemma (preliminary report), Type theory as a foundation for computer science, Some normalization properties of martin-löf's type theory, and applications, Intuitionistic completeness of first-order logic, Meaning explanations at higher dimension, From operational to denotational semantics, Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec, A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case, Unnamed Item, Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report), Proving the correctness of recursion-based automatic program transformations, Validating Brouwer's continuity principle for numbers using named exceptions, Process calculus based upon evaluation to committed form, On generic context lemmas for higher-order calculi with sharing, Formalizing Type Operations Using the “Image” Type Constructor, Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi, First–order Semantics for Higher–order Processes, Unnamed Item, From rewrite rules to bisimulation congruences, A Classical Realizability Model for a Semantical Value Restriction, Proving the correctness of recursion-based automatic program transformations, Exercising Nuprl’s Open-Endedness, Process calculus based upon evaluation to committed form, Using a generalisation critic to find bisimulations for coinductive proofs, Nuprl-Light: An implementation framework for higher-order logics, Syntactic Logical Relations for Polymorphic and Recursive Types, A co-induction principle for recursively defined domains, A fully abstract denotational semantics for the \(\pi\)-calculus, Untyped lambda-calculus with input-output
Uses Software
