LCF

swMATH8360MaRDI QIDQ20369FDOQ20369

Author name not available (Why is that?)

Official website: http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf

Described by source

• Edinburgh LCF. A mechanized logic of computation

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

• Unification: A case-study in data refinement
• Flyspeck II: The basic linear programs
• 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
• Logic programming with external procedures: Introducing S-unification
• Concrete domains
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Verifying the unification algorithm in LCF
• Proving and applying program transformations expressed with second-order patterns
• Title not available (Why is that?)
• An ideal model for recursive polymorphic types
• Sequential algorithms on concrete data structures
• Title not available (Why is that?)
• 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?)
• 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
• Proof checking and logic programming
• A formal proof of the Kepler conjecture
• 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
• A notation for lambda terms. A generalization of environments
• An efficient interpreter for the lambda-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Implementing type systems for the IDE with Xsemantics
• N. G. de Bruijn's contribution to the formalization of mathematics
• Writing programs that construct proofs
• Proof planning for strategy development
• Computability concepts for programming language semantics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Inductive methods for proving properties of programs
• Knowledge-based proof planning
• 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
• Title not available (Why is that?)
• The notion of proof in hardware verification
• ELAN from a rewriting logic point of view
• Proof assistants: history, ideas and future
• Computational foundations of basic recursive function theory
• Program Development in Computational Logic
• Some considerations on the usability of interactive provers
• A reflective functional language for hardware design and theorem proving
• Derivation of a parsing algorithm in Martin-Löf's theory of types
• Programs as proofs: A synopsis
• Reconstructing proofs at the assertion level
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Completeness results for the equivalence of recursive schemas
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Title not available (Why is that?)
• Title not available (Why is that?)
• On some classes of interpretations
• Toward an algebraic theory of systems
• Program transformations and algebraic semantics
• Proving termination of normalization functions for conditional expressions
• The promotion and accumulation strategies in transformational programming
• Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories
• Intuitionistic completeness of first-order logic
• Title not available (Why is that?)
• Automated proofs of object code for a widely used microprocessor
• A domain-theoretic model of nominally-typed object-oriented programming
• Notions of computation and monads
• Title not available (Why is that?)
• 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
• Productive use of failure in inductive proof
• Repairing time-determinism in the process algebra for hybrid systems
• Efficiently checking propositional refutations in HOL theorem provers
• A logic covering undefinedness in program proofs
• The IO- and OI-hierarchies
• Embedding complex decision procedures inside an interactive theorem prover.
• ML
• Isar
• MetaPRL
• Miranda
• HOL
• Matita
• OCaml
• Nuprl
• Automath
• Isabelle/PIDE
• NQTHM
• ALF

This page was built for software: LCF