The following pages link to LCF (Q20369):
Displaying 50 items.
- A domain-theoretic model of nominally-typed object-oriented programming (Q276420) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Repairing time-determinism in the process algebra for hybrid systems (Q442292) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- Implementing type systems for the IDE with Xsemantics (Q739624) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Type inference with recursive types: Syntax and semantics (Q756435) (← links)
- Notions of computation and monads (Q757075) (← links)
- Expressive power of typed and type-free programming languages (Q761790) (← links)
- A logic covering undefinedness in program proofs (Q790610) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Formal compiler construction in a logical framework (Q853741) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- A \(\rho\)-calculus of explicit constraint application (Q880989) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- The proof monad (Q974136) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Programs as proofs: A synopsis (Q1051424) (← links)
- Verifying the unification algorithm in LCF (Q1060023) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- Structured algebraic specifications: A kernel language (Q1080652) (← links)
- Derivation of a parsing algorithm in Martin-Löf's theory of types (Q1097045) (← links)
- Logic programming with external procedures: Introducing S-unification (Q1097682) (← links)
- Proving termination of normalization functions for conditional expressions (Q1101251) (← links)
- The notion of proof in hardware verification (Q1122998) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- CPO's of measures for nondeterminism (Q1139367) (← links)
- A mathematical semantics for a nondeterministic typed lambda-calculus (Q1152949) (← links)
- An efficient interpreter for the lambda-calculus (Q1158139) (← links)
- The IO- and OI-hierarchies (Q1161273) (← links)
- Sequential algorithms on concrete data structures (Q1170880) (← links)
- Algebraic system specification and development. A survey and annotated bibliography (Q1202052) (← links)
- Completeness results for the equivalence of recursive schemas (Q1232171) (← links)
- Computability concepts for programming language semantics (Q1235972) (← links)
- PASCAL in LCF: Semantics and examples of proof (Q1242670) (← links)
- LCF considered as a programming language (Q1243117) (← links)
- A theory of type polymorphism in programming (Q1250704) (← links)
- Proving and applying program transformations expressed with second-order patterns (Q1251063) (← links)
- On some classes of interpretations (Q1251892) (← links)
- Program transformations and algebraic semantics (Q1254849) (← links)
- Analytica --- an experiment in combining theorem proving and symbolic computation (Q1272608) (← links)
- Analogy in inductive theorem proving (Q1283199) (← links)
- The \(HOL\) logic extended with quantification over type variables (Q1309243) (← links)
- Experimenting with Isabelle in ZF set theory (Q1312157) (← links)
- Computational foundations of basic recursive function theory (Q1314348) (← links)
- Concrete domains (Q1314355) (← links)
