Logic and Computation
DOI10.1017/CBO9780511526602zbMATH Open0645.68041OpenAlexW4246059478WikidataQ57382737 ScholiaQ57382737MaRDI QIDQ3789060FDOQ3789060
Authors: Lawrence C. Paulson 
Publication date: 1987
Full work available at URL: https://doi.org/10.1017/cbo9780511526602
Recommendations
- Structural proof theory. With an appendix by Aarne Ranta
- Computational logic: its origins and applications
- Applied logic for computer scientists. Computational deduction and formal proofs
- scientific article; zbMATH DE number 5539366
- Fundamental proof methods in computer science. A computer-based approach
category theorydenotational semanticsmathematical logicreasoning about computationCambridge LCFPP\(\lambda \)recursive domains
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Classical first-order logic (03B10) Combinatory logic and lambda calculus (03B40) Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Computability and recursion theory (03D99) Proof theory and constructive mathematics (03F99)
Cited In (41)
- Codatatypes in ML
- Definition and basic properties of the Deva meta-calculus
- Theo: An interactive proof development system
- A fixedpoint approach to implementing (co)inductive definitions
- A framework for developing stand-alone certifiers
- A mechanisation of computability theory in HOL
- Synthetic domain theory in type theory: another logic of computable functions
- Winskel is (almost) right. Towards a mechanized semantics textbook
- Term rewriting and beyond -- theorem proving in Isabelle
- The foundation of a generic theorem prover
- Tactical theorem proving in program verification
- Title not available (Why is that?)
- Formal verification of a programming logic for a distributed programming language
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- Formalising Mathematics in Simple Type Theory
- The strategy challenge in SMT solving
- A fully automatic theorem prover with human-style output
- Reflection of formal tactics in a deductive reflection framework
- Proof synthesis and reflection for linear arithmetic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Experimenting with Isabelle in ZF set theory
- Foundations of a theorem prover for functional and mathematical uses
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Title not available (Why is that?)
- Cambridge LCF
- Nuprl-Light: An implementation framework for higher-order logics
- Dynamic modeling of branching morphogenesis of ureteric bud in early kidney development
- A tactic language for refinement of state-rich concurrent specifications
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
- A logic for Miranda
- Computational logic: its origins and applications
- Mechanizing a proof by induction of process algebra specifications in higher order logic
- Biological plausibility of synaptic associative memory models
- Structured theory presentations and logic representations
- Proof-search in type-theoretic languages: An introduction
- Proving Properties of Lazy Functional Programs with Sparkle
- A logic for Miranda, revisited
- From operational to denotational semantics
- A higher-order calculus and theory abstraction
- A theory of requirements capture and its applications
- R-calculus for ELP: An operational approach to knowledge base maintenance
Uses Software
This page was built for publication: Logic and Computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3789060)
