Logic and Computation

DOI10.1017/CBO9780511526602zbMath0645.68041OpenAlexW4246059478WikidataQ57382737 ScholiaQ57382737MaRDI QIDQ3789060

Lawrence Charles Paulson

Publication date: 1987

Full work available at URL: https://doi.org/10.1017/cbo9780511526602

zbMATH Keywords

category theorydenotational semanticsmathematical logicreasoning about computationCambridge LCFPP\(\lambda \)recursive domains

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Abstract data types; algebraic specification (68Q65) Classical first-order logic (03B10) Theories (e.g., algebraic theories), structure, and semantics (18C10) Computability and recursion theory (03D99) Combinatory logic and lambda calculus (03B40) Proof theory and constructive mathematics (03F99)

Related Items

Structured theory presentations and logic representations ⋮ A fully automatic theorem prover with human-style output ⋮ Dynamic modeling of branching morphogenesis of ureteric bud in early kidney development ⋮ A theory of requirements capture and its applications ⋮ Biological plausibility of synaptic associative memory models ⋮ Foundations of a theorem prover for functional and mathematical uses ⋮ A higher-order calculus and theory abstraction ⋮ A logic for Miranda, revisited ⋮ Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology ⋮ Computer assisted reasoning. A Festschrift for Michael J. C. Gordon ⋮ Formalising Mathematics in Simple Type Theory ⋮ From operational to denotational semantics ⋮ Codatatypes in ML ⋮ A logic for Miranda ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Proof synthesis and reflection for linear arithmetic ⋮ R-calculus for ELP: An operational approach to knowledge base maintenance ⋮ New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic ⋮ Reflection of formal tactics in a deductive reflection framework ⋮ The Strategy Challenge in SMT Solving ⋮ Theo: An interactive proof development system ⋮ Definition and basic properties of the Deva meta-calculus ⋮ A framework for developing stand-alone certifiers ⋮ A tactic language for refinement of state-rich concurrent specifications ⋮ Proving Properties of Lazy Functional Programs with Sparkle ⋮ A fixedpoint approach to implementing (Co)inductive definitions ⋮ Cambridge LCF ⋮ The foundation of a generic theorem prover ⋮ Nuprl-Light: An implementation framework for higher-order logics ⋮ Formal verification of a programming logic for a distributed programming language ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Experimenting with Isabelle in ZF set theory

Uses Software

• Miranda
• HOL
• Nuprl