scientific article; zbMATH DE number 4180818

MaRDI QIDQ3204055zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 1989

zbMATH Keywords

type theorieslazy computation systemsprogram equivalence in lazy languages

Mathematics Subject Classification ID

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)

Recommendations

• Lazy UTP
• Lazy Relations
• A complete axiomatization of strict equality
• Similarity-Based Equality with Lazy Evaluation
• Pure type systems with judgemental equality

Cited in

(42)

• From operational to denotational semantics
• Intuitionistic completeness of first-order logic
• Proving the correctness of recursion-based automatic program transformations
• 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
• A co-induction principle for recursively defined domains
• PML2: integrated program verification in ML
• From rewrite rules to bisimulation congruences
• First-order semantics for higher-order processes
• Process calculus based upon evaluation to committed form
• Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
• Process calculus based upon evaluation to committed form
• A complete axiomatization of strict equality
• Formalizing type operations using the ``image type constructor
• Exercising Nuprl's open-endedness
• Type theory as a foundation for computer science
• Quantitative logics for equivalence of effectful programs
• A Classical Realizability Model for a Semantical Value Restriction
• A fully abstract denotational semantics for the \(\pi\)-calculus
• Programming Languages and Systems
• Some normalization properties of Martin-Löf's type theory, and applications
• Untyped lambda-calculus with input-output
• Logical predicates in higher-order mathematical operational semantics
• Syntactic logical relations for polymorphic and recursive types
• Similarity-Based Equality with Lazy Evaluation
• Nuprl-Light: An implementation framework for higher-order logics
• Validating Brouwer's continuity principle for numbers using named exceptions
• Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
• A two-valued logic for properties of strict functional programs allowing partial functions
• Innovations in computational type theory using Nuprl
• Meaning explanations at higher dimension
• Howe's method for higher-order languages
• Two guarded recursive powerdomains for applicative simulation
• A theory of bisimulation for a fragment of concurrent ML with local names
• Full abstraction and the Context Lemma (preliminary report)
• Labelled reductions, runtime errors, and operational subsumption
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• 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
• Proving the correctness of recursion-based automatic program transformations

Describes a project that uses

Uses Software

• Nuprl

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)