LCF

swMATH8360MaRDI QIDQ20369

No author found.

Described by source

• Edinburgh LCF. A mechanized logic of computation

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

A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Transparent optimisation of rewriting combinators ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Programming Combinations of Deduction and BDD-based Symbolic Calculation ⋮ Structuring metatheory on inductive definitions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An ideal model for recursive polymorphic types ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Logical Analysis of Hybrid Systems ⋮ Operational interpretations of an extension of F_ω with control operators ⋮ Preface ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Étude et implémentation d'un système de déduction pour logique algorithmique ⋮ Unnamed Item ⋮ Automated proofs of object code for a widely used microprocessor ⋮ Program Development in Computational Logic ⋮ Unnamed Item ⋮ Internal analogy in theorem proving ⋮ Reflection of formal tactics in a deductive reflection framework ⋮ The Strategy Challenge in SMT Solving ⋮ Unnamed Item ⋮ The promotion and accumulation strategies in transformational programming ⋮ Some Considerations on the Usability of Interactive Provers ⋮ Lucid—A Formal System for Writing and Proving Programs ⋮ Inductive methods for proving properties of programs ⋮ Recursive Programs as Definitions in First-Order Logic ⋮ The Watson theorem prover ⋮ The control layer in open mechanized reasoning systems: Annotations and tactics ⋮ Unnamed Item ⋮ A formal proof of the expressiveness of deep learning ⋮ A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL ⋮ Unnamed Item ⋮ Tactic theorem proving with refinement-tree proofs and metavariables ⋮ Reconstructing proofs at the assertion level ⋮ Unnamed Item ⋮ A reflective functional language for hardware design and theorem proving ⋮ Unnamed Item ⋮ Efficient verified (UN)SAT certificate checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC ⋮ Unnamed Item ⋮ Structured algebraic specifications: A kernel language ⋮ A domain-theoretic model of nominally-typed object-oriented programming ⋮ Verification methods: Rigorous results using floating-point arithmetic ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Eisbach: a proof method language for Isabelle ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Proof checking and logic programming ⋮ Derivation of a parsing algorithm in Martin-Löf's theory of types ⋮ Challenges and Experiences in Managing Large-Scale Proofs ⋮ Flyspeck II: The basic linear programs ⋮ Logic programming with external procedures: Introducing S-unification ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ Unification: A case-study in data refinement ⋮ Some Domain Theory and Denotational Semantics in Coq ⋮ Proving termination of normalization functions for conditional expressions ⋮ Standalone Tactics Using OpenTheory ⋮ Formal compiler construction in a logical framework ⋮ Innovations in computational type theory using Nuprl ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Unnamed Item ⋮ Formalization of the resolution calculus for first-order logic ⋮ Productive use of failure in inductive proof ⋮ An algorithm for type-checking dependent types ⋮ Unnamed Item ⋮ The notion of proof in hardware verification ⋮ Using tactics to reformulate formulae for resolution theorem proving ⋮ Program tactics and logic tactics ⋮ A \(\rho\)-calculus of explicit constraint application ⋮ A notation for lambda terms. A generalization of environments ⋮ Intuitionistic completeness of first-order logic ⋮ Unnamed Item ⋮ A metatheory of a mechanized object theory ⋮ CPO's of measures for nondeterminism ⋮ A semantic framework for proof evidence ⋮ A mathematical semantics for a nondeterministic typed lambda-calculus ⋮ An efficient interpreter for the lambda-calculus ⋮ Repairing time-determinism in the process algebra for hybrid systems ⋮ The IO- and OI-hierarchies ⋮ Formal verification of a partial-order reduction technique for model checking ⋮ Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving ⋮ Sequential algorithms on concrete data structures ⋮ Realizability and Parametricity in Pure Type Systems ⋮ Knowledge-based proof planning

This page was built for software: LCF