Logic and Computation
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)
- 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
- From operational to denotational semantics
- A theory of requirements capture and its applications
- Codatatypes in ML
- Definition and basic properties of the Deva meta-calculus
- Theo: An interactive proof development system
- A framework for developing stand-alone certifiers
- A fixedpoint approach to implementing (co)inductive definitions
- 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
- Formal verification of a programming logic for a distributed programming language
- Tactical theorem proving in program verification
- scientific article; zbMATH DE number 1531624 (Why is no real title available?)
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- A fully automatic theorem prover with human-style output
- Formalising Mathematics in Simple Type Theory
- The strategy challenge in SMT solving
- 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
- Cambridge LCF
- Foundations of a theorem prover for functional and mathematical uses
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- scientific article; zbMATH DE number 4072441 (Why is no real title available?)
- Dynamic modeling of branching morphogenesis of ureteric bud in early kidney development
- A tactic language for refinement of state-rich concurrent specifications
- Nuprl-Light: An implementation framework for higher-order logics
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
- A logic for Miranda
- Computational logic: its origins and applications
- Biological plausibility of synaptic associative memory models
- Mechanizing a proof by induction of process algebra specifications in higher order logic
- 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
- R-calculus for ELP: An operational approach to knowledge base maintenance
- A higher-order calculus and theory abstraction
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)
