LCF

swMATH8360MaRDI QIDQ20369FDOQ20369

Author name not available (Why is that?)

Described by source

• Edinburgh LCF. A mechanized logic of computation

Cited In (only showing first 100 items - show all)

• Intuitionistic completeness of first-order logic
• Flyspeck II: The basic linear programs
• Title not available (Why is that?)
• A framework for developing stand-alone certifiers
• Type inference with recursive types: Syntax and semantics
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• Formal verification of a partial-order reduction technique for model checking
• A mathematical semantics for a nondeterministic typed lambda-calculus
• Automated proofs of object code for a widely used microprocessor
• Some Considerations on the Usability of Interactive Provers
• Concrete domains
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• A domain-theoretic model of nominally-typed object-oriented programming
• Logical Analysis of Hybrid Systems
• Proving and applying program transformations expressed with second-order patterns
• Notions of computation and monads
• Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture
• An ideal model for recursive polymorphic types
• Sequential algorithms on concrete data structures
• Termination of Isabelle Functions via Termination of Rewriting
• The proof monad
• Consistent and complementary formal theories of the semantics of programming languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal compiler construction in a logical framework
• Recursive Programs as Definitions in First-Order Logic
• Formalization of the resolution calculus for first-order logic
• A \(\rho\)-calculus of explicit constraint application
• Eisbach: a proof method language for Isabelle
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• LCF considered as a programming language
• Lightweight static capabilities
• Lucid—A Formal System for Writing and Proving Programs
• Structured algebraic specifications: A kernel language
• CPO's of measures for nondeterminism
• Computer theorem proving in mathematics
• Some Domain Theory and Denotational Semantics in Coq
• Productive use of failure in inductive proof
• Repairing time-determinism in the process algebra for hybrid systems
• Title not available (Why is that?)
• Efficiently checking propositional refutations in HOL theorem provers
• Title not available (Why is that?)
• A logic covering undefinedness in program proofs
• Implementing type systems for the IDE with Xsemantics
• N. G. de Bruijn's contribution to the formalization of mathematics
• Writing programs that construct proofs
• Computability concepts for programming language semantics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The IO- and OI-hierarchies
• Embedding complex decision procedures inside an interactive theorem prover.
• Inductive methods for proving properties of programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards a computation system based on set theory
• Expressive power of typed and type-free programming languages
• An algorithm for type-checking dependent types
• The notion of proof in hardware verification
• ELAN from a rewriting logic point of view
• Computational foundations of basic recursive function theory
• Innovations in computational type theory using Nuprl
• Program Development in Computational Logic
• Computational effects and operations: an overview
• Verification methods: rigorous results using floating-point arithmetic
• The Watson theorem prover
• A reflective functional language for hardware design and theorem proving
• A theory of type polymorphism in programming
• Analogy in inductive theorem proving
• OBSCURE, a specification language for abstract data types
• Programs as proofs: A synopsis
• Reconstructing proofs at the assertion level
• Partial and nested recursive function definitions in higher-order logic
• Preface
• Challenges and Experiences in Managing Large-Scale Proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Synthesis of ML programs in the system Coq
• On some classes of interpretations
• Program transformations and algebraic semantics
• Proving termination of normalization functions for conditional expressions
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Title not available (Why is that?)
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Unification: A case-study in data refinement
• Structuring metatheory on inductive definitions
• Étude et implémentation d'un système de déduction pour logique algorithmique
• PASCAL in LCF: Semantics and examples of proof
• Title not available (Why is that?)
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Logic programming with external procedures: Introducing S-unification
• Relative definability of boolean functions via hypergraphs
• Title not available (Why is that?)
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Verifying the unification algorithm in LCF
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A proof dedicated meta-language

This page was built for software: LCF