Pages that link to "Item:Q1801222"
From MaRDI portal
The following pages link to Edinburgh LCF. A mechanized logic of computation (Q1801222):
Displaying 50 items.
- LCF (Q20369) (← links)
- A domain-theoretic model of nominally-typed object-oriented programming (Q276420) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Conjecture synthesis for inductive theories (Q438543) (← links)
- Automatic verification of reduction techniques in higher order logic (Q469363) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- A tactic language for refinement of state-rich concurrent specifications (Q541214) (← links)
- Tactics for hierarchical proof (Q626933) (← links)
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation (Q651316) (← links)
- Automated theorem provers: a practical tool for the working mathematician? (Q657585) (← links)
- Intersection type assignment systems with higher-order algebraic rewriting (Q672048) (← links)
- A type soundness proof for variables in LCF ML (Q672255) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Extensional models for polymorphism (Q749518) (← links)
- Functorial polymorphism (Q753948) (← links)
- Type inference with recursive types: Syntax and semantics (Q756435) (← links)
- Notions of computation and monads (Q757075) (← links)
- Semantics of interference control (Q759473) (← links)
- A logic covering undefinedness in program proofs (Q790610) (← links)
- Experiments with proof plans for induction (Q809617) (← 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)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- A few exercises in theorem processing (Q879370) (← links)
- A \(\rho\)-calculus of explicit constraint application (Q880989) (← links)
- Codatatypes in ML (Q908682) (← links)
- A functional programming approach to the specification and verification of concurrent systems (Q909439) (← links)
- Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
- Constructive system for automatic program synthesis (Q912589) (← links)
- Refinement concepts formalised in higher order logic (Q916409) (← links)
- Type inference for polymorphic references (Q918190) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- The proof monad (Q974136) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Programs as proofs: A synopsis (Q1051424) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- Structured algebraic specifications: A kernel language (Q1080652) (← links)
- Inserting injection operations to denotational specifications (Q1082803) (← links)
- Scott induction and closure under \(\omega\)-sups (Q1087326) (← links)
- Constructing recursion operators in intuitionistic type theory (Q1094421) (← links)
- Needed reduction and spine strategies for the lambda calculus (Q1097253) (← links)
- Logic programming with external procedures: Introducing S-unification (Q1097682) (← links)
- Recursively defined domains and their induction principles (Q1098615) (← links)
- Pebble, a kernel language for modules and abstract data types (Q1104071) (← links)
- The calculus of constructions (Q1108266) (← links)
