Pages that link to "Item:Q5777498"

The following pages link to A formulation of the simple theory of types (Q5777498):

Displaying 50 items.

• Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
• Functorial semantics of first-order views (Q344796) (← links)
• Analytic tableaux for higher-order logic with choice (Q438561) (← links)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
• Bounded memory Dolev-Yao adversaries in collaborative systems (Q462499) (← links)
• Structured derivations: a unified proof style for teaching mathematics (Q607406) (← links)
• Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
• Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
• A simple proof that super-consistency implies cut elimination (Q691121) (← links)
• A higher-order theory of presupposition (Q692197) (← links)
• A framework for proof systems (Q707742) (← links)
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
• CERES in higher-order logic (Q716500) (← links)
• Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
• Probabilistic modelling, inference and learning using logical theories (Q841641) (← links)
• Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
• Expressing combinatory reduction systems derivations in the rewriting calculus (Q857913) (← links)
• On connections and higher-order logic (Q908896) (← links)
• Formalizing non-interference for a simple bytecode language in Coq (Q931434) (← links)
• Adapting functional programs to higher order logic (Q1029815) (← links)
• Using theorem proving to verify expectation and variance for discrete random variables (Q1040780) (← links)
• A compact representation of proofs (Q1102282) (← links)
• Intuitionist type theory and foundations (Q1152364) (← links)
• A completeness theorem for the general interpreted modal calculus MC**nu of A. Bressan (Q1163535) (← links)
• Lambek calculus with restricted contraction and expansion (Q1194112) (← links)
• Types with intersection: An introduction (Q1201298) (← links)
• Expressibility of propositions in \(L_\mu\)-languages (Q1211043) (← links)
• Adverbs and events (Q1217695) (← links)
• A unification algorithm for typed \(\bar\lambda\)-calculus (Q1227601) (← links)
• The \(HOL\) logic extended with quantification over type variables (Q1309243) (← links)
• Lazy techniques for fully expansive theorem proving (Q1309245) (← links)
• Mechanizing some advanced refinement concepts (Q1309250) (← links)
• Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
• What holds in a context? (Q1312161) (← links)
• A type-theoretical alternative to ISWIM, CUCH, OWHY (Q1314363) (← links)
• IMPS: An interactive mathematical proof system (Q1319391) (← links)
• Annotations in formal specifications and proofs (Q1334901) (← links)
• Using tactics to reformulate formulae for resolution theorem proving (Q1380410) (← links)
• Intertheoretic reduction, confirmation, and Montague's syntax-semantics relation (Q1630947) (← links)
• The Cooper storage idiom (Q1711505) (← links)
• Semantic bootstrapping of type-logical grammar (Q1778102) (← links)
• TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
• Carnap, Goguen, and the hyperontologies: logical pluralism and heterogeneous structuring in ontology design (Q1931353) (← links)
• Embedding and automating conditional logics in classical higher-order logic (Q1935597) (← links)
• Quantified multimodal logics in simple type theory (Q1945702) (← links)
• Semantics of \textsc{OpenMath} and \textsc{MathML3} (Q1948675) (← links)
• Grammar induction by unification of type-logical lexicons (Q1959226) (← links)
• Filter quotients and non-presentable \((\infty,1)\)-toposes (Q2040521) (← links)
• A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
• Meaning and computing: two approaches to computable propositions (Q2148782) (← links)