Logic and Computation
Cambridge LCFcategory theorydenotational semanticsmathematical logicPP\(\lambda \)reasoning about computationrecursive domains
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Classical first-order logic (03B10) Combinatory logic and lambda calculus (03B40) Computability and recursion theory (03D99) Proof theory and constructive mathematics (03F99) Theories (e.g., algebraic theories), structure, and semantics (18C10) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Abstract data types; algebraic specification (68Q65)
- 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
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
- Formal verification of a programming logic for a distributed programming language
- Experimenting with Isabelle in ZF set theory
- Structured theory presentations and logic representations
- Biological plausibility of synaptic associative memory models
- Proof-search in type-theoretic languages: An introduction
- Dynamic modeling of branching morphogenesis of ureteric bud in early kidney development
- The foundation of a generic theorem prover
- A logic for Miranda, revisited
- A fully automatic theorem prover with human-style output
- A higher-order calculus and theory abstraction
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Proving Properties of Lazy Functional Programs with Sparkle
- scientific article; zbMATH DE number 4072441 (Why is no real title available?)
- Foundations of a theorem prover for functional and mathematical uses
- Cambridge LCF
- scientific article; zbMATH DE number 1531624 (Why is no real title available?)
- Computational logic: its origins and applications
- Reflection of formal tactics in a deductive reflection framework
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- The strategy challenge in SMT solving
- A theory of requirements capture and its applications
- A fixedpoint approach to implementing (co)inductive definitions
- Nuprl-Light: An implementation framework for higher-order logics
- A framework for developing stand-alone certifiers
- A tactic language for refinement of state-rich concurrent specifications
- Formalising Mathematics in Simple Type Theory
- From operational to denotational semantics
- Tactical theorem proving in program verification
- Mechanizing a proof by induction of process algebra specifications in higher order logic
- Synthetic domain theory in type theory: another logic of computable functions
- A mechanisation of computability theory in HOL
- Winskel is (almost) right. Towards a mechanized semantics textbook
- R-calculus for ELP: An operational approach to knowledge base maintenance
- A denotationally-based program logic for higher-order store
- Theo: An interactive proof development system
- Definition and basic properties of the Deva meta-calculus
- Translating HOL-Light proofs to Coq
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Codatatypes in ML
- A logic for Miranda
- Term rewriting and beyond -- theorem proving in Isabelle
- Proof synthesis and reflection for linear arithmetic
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)
