Edinburgh LCF. A mechanized logic of computation

zbMath0421.68039MaRDI QIDQ1801222

Arthur J. Milner, Christopher P. Wadsworth, Michael J. C. Gordon

Publication date: 5 June 1993

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

algorithmsprogramming languagesnatural deductionprogramsdeductive calculigoal-directed proof procedureslogic for computable functionsprogramming metalanguagereference manual for the implemented systems

Mathematics Subject Classification ID

Related Items (only showing first 100 items - show all)

A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Transfer of Model Checking to Industrial Practice ⋮ Unifying Theories of Undefinedness in UTP ⋮ ProofScript: Proof Scripting for the Masses ⋮ Without Loss of Generality ⋮ HOL Light: An Overview ⋮ Computational logic: its origins and applications ⋮ Structuring metatheory on inductive definitions ⋮ Parallélisation sémantique ⋮ Type theory as a foundation for computer science ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ A metatheory of a mechanized object theory ⋮ A Declarative Language for the Coq Proof Assistant ⋮ On extensibility of proof checkers ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ The Alf proof editor and its proof engine ⋮ From operational to denotational semantics ⋮ The formal verification of the ctm approach to forcing ⋮ Efficient extensional binary tries ⋮ Formalization of the inverse kinematics of three-fingered dexterous hand ⋮ Unnamed Item ⋮ Hoare logic for Java in Isabelle/HOL ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ No value restriction is needed for algebraic effects and handlers ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Étude et implémentation d'un système de déduction pour logique algorithmique ⋮ The Isabelle Framework ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Extensions to a generalization critic for inductive proof ⋮ Internal analogy in theorem proving ⋮ Reflection of formal tactics in a deductive reflection framework ⋮ Proof Checking and Logic Programming ⋮ Proving Properties of Lazy Functional Programs with Sparkle ⋮ The control layer in open mechanized reasoning systems: Annotations and tactics ⋮ A formal proof of the expressiveness of deep learning ⋮ Proof script pragmatics in IMPS ⋮ Tactic theorem proving with refinement-tree proofs and metavariables ⋮ Reconstructing proofs at the assertion level ⋮ Mollusc a general proof-development shell for sequent-based logics ⋮ Scalable fine-grained proofs for formula processing ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Validating QBF Validity in HOL4 ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers ⋮ LCF-style Platform based on Multiway Decision Graphs ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time ⋮ Hybrid interactive theorem proving using nuprl and HOL ⋮ Proof Auditing Formalised Mathematics ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC ⋮ Tinycals: Step by Step Tacticals ⋮ Structured theory presentations and logic representations ⋮ Structured algebraic specifications: A kernel language ⋮ A domain-theoretic model of nominally-typed object-oriented programming ⋮ Inserting injection operations to denotational specifications ⋮ Rule-based induction ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Eisbach: a proof method language for Isabelle ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Scott induction and closure under \(\omega\)-sups ⋮ On the \(\lambda Y\) calculus ⋮ An overview of the Tecton proof system ⋮ Proof checking and logic programming ⋮ Speedith: a reasoner for spider diagrams ⋮ Constructing recursion operators in intuitionistic type theory ⋮ Needed reduction and spine strategies for the lambda calculus ⋮ Logic programming with external procedures: Introducing S-unification ⋮ Recursively defined domains and their induction principles ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ Formal compiler construction in a logical framework ⋮ Pebble, a kernel language for modules and abstract data types ⋮ The calculus of constructions ⋮ Polymorphic type inference and containment ⋮ Innovations in computational type theory using Nuprl ⋮ Computer assisted reasoning. A Festschrift for Michael J. C. Gordon ⋮ Formalizing an analytic proof of the prime number theorem ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Productive use of failure in inductive proof ⋮ Middle-out reasoning for synthesis and induction ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Program tactics and logic tactics ⋮ Providing a formal linkage between MDG and HOL ⋮ A few exercises in theorem processing ⋮ TPS: A theorem-proving system for classical type theory ⋮ A \(\rho\)-calculus of explicit constraint application ⋮ A notation for lambda terms. A generalization of environments ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Intuitionistic completeness of first-order logic ⋮ A linear logical framework ⋮ Tactics for hierarchical proof ⋮ Unifying theories in ProofPower-Z ⋮ A semantic framework for proof evidence ⋮ Codatatypes in ML ⋮ A functional programming approach to the specification and verification of concurrent systems ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Conjecture synthesis for inductive theories

This page was built for publication: Edinburgh LCF. A mechanized logic of computation