scientific article; zbMATH DE number 4180818

MaRDI QIDQ3204055zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 1989

zbMATH Keywords

lazy computation systemsprogram equivalence in lazy languagestype theories

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

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

(44)

• Process calculus based upon evaluation to committed form
• A co-induction principle for recursively defined domains
• On reduction-based process semantics
• A fully abstract denotational semantics for the \(\pi\)-calculus
• Meaning explanations at higher dimension
• A theory of bisimulation for a fragment of concurrent ML with local names
• Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
• Quantitative logics for equivalence of effectful programs
• A Classical Realizability Model for a Semantical Value Restriction
• Exercising Nuprl's open-endedness
• Syntactic logical relations for polymorphic and recursive types
• Similarity-Based Equality with Lazy Evaluation
• A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case
• A two-valued logic for properties of strict functional programs allowing partial functions
• A complete axiomatization of strict equality
• Intuitionistic completeness of first-order logic
• Labelled reductions, runtime errors, and operational subsumption
• Validating Brouwer's continuity principle for numbers using named exceptions
• Formalizing type operations using the ``image type constructor
• First-order semantics for higher-order processes
• A cubical language for Bishop sets
• 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
• Proving the correctness of recursion-based automatic program transformations
• The functional interpretation of direct computations
• Using a generalisation critic to find bisimulations for coinductive proofs
• Nuprl-Light: An implementation framework for higher-order logics
• Contextual equivalences in call-by-need and call-by-name polymorphically typed calculi (preliminary report)
• Programming Languages and Systems
• Howe's method for higher-order languages
• Untyped lambda-calculus with input-output
• From rewrite rules to bisimulation congruences
• PML2: integrated program verification in ML
• Process calculus based upon evaluation to committed form
• From operational to denotational semantics
• Logical predicates in higher-order mathematical operational semantics
• Two guarded recursive powerdomains for applicative simulation
• Proving the correctness of recursion-based automatic program transformations
• Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle
• Bialgebraic reasoning on higher-order program equivalence
• Innovations in computational type theory using Nuprl
• On generic context lemmas for higher-order calculi with sharing
• Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi

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)