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 (35)
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
This page was built for publication:
