LCF
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Intuitionistic completeness of first-order logic
- Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories
- Internal analogy in theorem proving
- Unification: A case-study in data refinement
- Structuring metatheory on inductive definitions
- Flyspeck II: The basic linear programs
- PASCAL in LCF: Semantics and examples of proof
- Étude et implémentation d'un système de déduction pour logique algorithmique
- A framework for developing stand-alone certifiers
- scientific article; zbMATH DE number 3985475 (Why is no real title available?)
- Type inference with recursive types: Syntax and semantics
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- scientific article; zbMATH DE number 3439981 (Why is no real title available?)
- A mathematical semantics for a nondeterministic typed lambda-calculus
- Logic programming with external procedures: Introducing S-unification
- Formal verification of a partial-order reduction technique for model checking
- Relative definability of boolean functions via hypergraphs
- Practical theory extension in Event-B
- Automated proofs of object code for a widely used microprocessor
- 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
- Verifying the unification algorithm in LCF
- Proving and applying program transformations expressed with second-order patterns
- scientific article; zbMATH DE number 1235907 (Why is no real title available?)
- Programming Combinations of Deduction and BDD-based Symbolic Calculation
- Notions of computation and monads
- scientific article; zbMATH DE number 1863374 (Why is no real title available?)
- Sequential algorithms on concrete data structures
- scientific article; zbMATH DE number 7649970 (Why is no real title available?)
- An ideal model for recursive polymorphic types
- The proof monad
- A proof dedicated meta-language
- Completeness in PVS of a nominal unification algorithm
- scientific article; zbMATH DE number 3991419 (Why is no real title available?)
- Mechanized metatheory revisited
- Consistent and complementary formal theories of the semantics of programming languages
- Validating QBF Validity in HOL4
- Formal compiler construction in a logical framework
- scientific article; zbMATH DE number 3553737 (Why is no real title available?)
- A \(\rho\)-calculus of explicit constraint application
- Formalization of the resolution calculus for first-order logic
- scientific article; zbMATH DE number 3967898 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- Analytica --- an experiment in combining theorem proving and symbolic computation
- Eisbach: a proof method language for Isabelle
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Recursive Programs as Definitions in First-Order Logic
- Efficient verified (UN)SAT certificate checking
- LCF considered as a programming language
- Proof checking and logic programming
- A formal framework for managing mathematics
- Operational interpretations of an extension of Fω with control operators
- The strategy challenge in SMT solving
- Structured algebraic specifications: A kernel language
- Lightweight static capabilities
- A formal proof of the Kepler conjecture
- Lucid—A Formal System for Writing and Proving Programs
- CPO's of measures for nondeterminism
- Computer theorem proving in mathematics
- Repairing time-determinism in the process algebra for hybrid systems
- A notation for lambda terms. A generalization of environments
- Productive use of failure in inductive proof
- An efficient interpreter for the lambda-calculus
- Reflection of formal tactics in a deductive reflection framework
- Some Domain Theory and Denotational Semantics in Coq
- Guest editors' preface to special issue on interval temporal logics
- Efficiently checking propositional refutations in HOL theorem provers
- 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
- scientific article; zbMATH DE number 1497752 (Why is no real title available?)
- scientific article; zbMATH DE number 3410594 (Why is no real title available?)
- Writing programs that construct proofs
- Realizability and parametricity in pure type systems
- Proof planning for strategy development
- The \(HOL\) logic extended with quantification over type variables
- Experimenting with Isabelle in ZF set theory
- Computability concepts for programming language semantics
- The IO- and OI-hierarchies
- scientific article; zbMATH DE number 3474961 (Why is no real title available?)
- Isabelle
- ALGOL 68
- ML
- ELAN
- OBSCURE
- Isar
- MetaPRL
- Miranda
- HOL
- Matita
- OCaml
- Nuprl
- Automath
- Isabelle/PIDE
- NQTHM
- ALF
- IMPS
- ValEncIA
- Bedwyr
This page was built for software: LCF
