swMATH8360MaRDI QIDQ20369FDOQ20369
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf
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
