Cited in
(only showing first 100 items - show all)- Synthesis of ML programs in the system Coq
- Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
- A theory of type polymorphism in programming
- A domain-theoretic model of nominally-typed object-oriented programming
- Intuitionistic completeness of first-order logic
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- The IO- and OI-hierarchies
- Efficiently checking propositional refutations in HOL theorem provers
- Computational effects and operations: an overview
- Interactive theorem proving from the perspective of Isabelle/Isar
- scientific article; zbMATH DE number 67450 (Why is no real title available?)
- Eisbach: a proof method language for Isabelle
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Analogy in inductive theorem proving
- Preface to the special issue: Interactive theorem proving and the formalization of mathematics
- Challenges and experiences in managing large-scale proofs
- scientific article; zbMATH DE number 3985475 (Why is no real title available?)
- Productive use of failure in inductive proof
- A logic covering undefinedness in program proofs
- LCF considered as a programming language
- Innovations in computational type theory using Nuprl
- Verification methods: rigorous results using floating-point arithmetic
- Embedding complex decision procedures inside an interactive theorem prover.
- Notions of computation and monads
- Isabelle
- ALGOL 68
- ML
- ELAN
- OBSCURE
- Isar
- MetaPRL
- Miranda
- HOL
- Matita
- OCaml
- Nuprl
- Automath
- Isabelle/PIDE
- NQTHM
- ALF
- IMPS
- ValEncIA
- Bedwyr
- Minlog
- Squolem
- Milawa
- PhoX
- IsaFoR
- Analytica
- MDGs
- Jitawa
- Eisbach
- Mtac
- Camlp4
- The Watson theorem prover
- CLAM
- MKRP
- Elf
- SPEC
- Lucid
- ALGOL 60
- Horus
- Teyjus
- kepler98
- GETFOL
- Watson
- YACC
- ELPI
- Depth First Search
- MadMax
- Psyche
- MAGMA-Lisp
- Presburger Automata
- EVES
- Haskell Show Class
- Coccinelle
- Centaur
- Xml
- Omega-MKRP
- PRIZ
- XIsabelle
- Cambridge LCF
- Certification_Monads
- DefunT
- Groebner_Bases
- Group-Ring-Module
- Matrix_Tensor
- Jape
- OpenTheory
- TXDT
- Ruler
- TALx86
- OBSCURE, a specification language for abstract data types
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- Partial and nested recursive function definitions in higher-order logic
- Termination of Isabelle functions via termination of rewriting
- Standalone Tactics Using OpenTheory
- The control layer in open mechanized reasoning systems: Annotations and tactics
- Wetzels_Problem
- scientific article; zbMATH DE number 3553737 (Why is no real title available?)
This page was built for software: LCF
