scientific article; zbMATH DE number 4180818
From MaRDI portal
Publication:3204055
zbMATH Open0716.68065MaRDI QIDQ3204055FDOQ3204055
Authors: Douglas J. Howe 
Publication date: 1989
Title of this publication is not available (Why is that?)
Recommendations
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35)
Cited In (42)
- Intuitionistic completeness of first-order logic
- A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case
- Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi
- The functional interpretation of direct computations
- PML2: integrated program verification in ML
- A co-induction principle for recursively defined domains
- From rewrite rules to bisimulation congruences
- First-order semantics for higher-order processes
- Process calculus based upon evaluation to committed form
- Process calculus based upon evaluation to committed form
- Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
- A complete axiomatization of strict equality
- Formalizing type operations using the ``image type constructor
- Type theory as a foundation for computer science
- Exercising Nuprl's open-endedness
- Quantitative logics for equivalence of effectful programs
- Programming Languages and Systems
- A Classical Realizability Model for a Semantical Value Restriction
- Some normalization properties of Martin-Löf's type theory, and applications
- A fully abstract denotational semantics for the \(\pi\)-calculus
- Untyped lambda-calculus with input-output
- Logical predicates in higher-order mathematical operational semantics
- Nuprl-Light: An implementation framework for higher-order logics
- Syntactic logical relations for polymorphic and recursive types
- Similarity-Based Equality with Lazy Evaluation
- Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
- Validating Brouwer's continuity principle for numbers using named exceptions
- A two-valued logic for properties of strict functional programs allowing partial functions
- Innovations in computational type theory using Nuprl
- Howe's method for higher-order languages
- Two guarded recursive powerdomains for applicative simulation
- Meaning explanations at higher dimension
- Full abstraction and the Context Lemma (preliminary report)
- A theory of bisimulation for a fragment of concurrent ML with local names
- Labelled reductions, runtime errors, and operational subsumption
- Title not available (Why is that?)
- On generic context lemmas for higher-order calculi with sharing
- On reduction-based process semantics
- Using a generalisation critic to find bisimulations for coinductive proofs
- From operational to denotational semantics
- Proving the correctness of recursion-based automatic program transformations
- Proving the correctness of recursion-based automatic program transformations
Uses Software
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 Q3204055)
