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)

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

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)