LCF
From MaRDI portal
Software:20369
swMATH8360MaRDI QIDQ20369FDOQ20369
Author name not available (Why is that?)
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