LCF
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Efficiently checking propositional refutations in HOL theorem provers
- Proof assistants: history, ideas and future
- Programs as proofs: A synopsis
- Verifying the unification algorithm in LCF
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Structured algebraic specifications: A kernel language
- Derivation of a parsing algorithm in Martin-Löf's theory of types
- Logic programming with external procedures: Introducing S-unification
- Proving termination of normalization functions for conditional expressions
- The notion of proof in hardware verification
- A notation for lambda terms. A generalization of environments
- CPO's of measures for nondeterminism
- A mathematical semantics for a nondeterministic typed lambda-calculus
- An efficient interpreter for the lambda-calculus
- The IO- and OI-hierarchies
- Sequential algorithms on concrete data structures
- Algebraic system specification and development. A survey and annotated bibliography
- Completeness results for the equivalence of recursive schemas
- Computability concepts for programming language semantics
- PASCAL in LCF: Semantics and examples of proof
- LCF considered as a programming language
- A theory of type polymorphism in programming
- Proving and applying program transformations expressed with second-order patterns
- On some classes of interpretations
- Program transformations and algebraic semantics
- Analytica --- an experiment in combining theorem proving and symbolic computation
- Analogy in inductive theorem proving
- The \(HOL\) logic extended with quantification over type variables
- Experimenting with Isabelle in ZF set theory
- Computational foundations of basic recursive function theory
- Concrete domains
- Isabelle
- Synthesis of ML programs in the system Coq
- OBSCURE, a specification language for abstract data types
- Jukebox
- Embedding complex decision procedures inside an interactive theorem prover.
- Using tactics to reformulate formulae for resolution theorem proving
- Program tactics and logic tactics
- ML
- ALGOL 68
- ELAN
- OBSCURE
- Proof planning for strategy development
- Relative definability of boolean functions via hypergraphs
- ELAN from a rewriting logic point of view
- Formalization of the resolution calculus for first-order logic
- Isar
- MetaPRL
- A semantic framework for proof evidence
- Miranda
- Completeness in PVS of a nominal unification algorithm
- HOL
- Toward an algebraic theory of systems
- Writing programs that construct proofs
- Towards a computation system based on set theory
- Matita
- OCaml
- Structuring metatheory on inductive definitions
- Nuprl
- Unification: A case-study in data refinement
- Productive use of failure in inductive proof
- An algorithm for type-checking dependent types
- Automath
- Isabelle/PIDE
- NQTHM
- Formal verification of a partial-order reduction technique for model checking
- Knowledge-based proof planning
- Twee: an equational theorem prover
- ALF
- ValEncIA
- IMPS
- Squolem
- Bedwyr
- Minlog
- PhoX
- Milawa
- IsaFoR
- Analytica
- Guest editors' preface to special issue on interval temporal logics
- From LCF to Isabelle/HOL
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Mechanized metatheory revisited
- Flyspeck II: The basic linear programs
- MDGs
- Jitawa
- Mtac
- Eisbach
- Consistent and complementary formal theories of the semantics of programming languages
- Proof checking and logic programming
- Crystal: Integrating structured queries into a tactic language
- A metatheory of a mechanized object theory
- Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories
- A domain-theoretic model of nominally-typed object-oriented programming
- A formal framework for managing mathematics
- HOL Zero's solutions for Pollack-inconsistency
- Incompleteness, Undecidability and Automated Proofs
- Practical theory extension in Event-B
- A proof dedicated meta-language
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Computational effects and operations: an overview
This page was built for software: LCF
