Pages that link to "Item:Q688571"

The following pages link to Using typed lambda calculus to implement formal systems on a machine (Q688571):

Displaying 35 items.

• Forum: A multiple-conclusion specification logic (Q671512) (← links)
• Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
• Theo: An interactive proof development system (Q688727) (← links)
• Mechanizing type environments in weak HOAS (Q897934) (← links)
• The semantics and proof theory of linear logic (Q1106836) (← links)
• Structured theory presentations and logic representations (Q1326777) (← links)
• A first order logic of effects (Q1390955) (← links)
• Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
• \(\pi\)-calculus in (Co)inductive-type theory (Q1589654) (← links)
• The foundation of a generic theorem prover (Q1823013) (← links)
• Structuring metatheory on inductive definitions (Q1854368) (← links)
• On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions (Q1854404) (← links)
• A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931) (← links)
• Twenty years of rewriting logic (Q1931904) (← links)
• A type-theoretic approach to program development (Q2277827) (← links)
• Term-generic logic (Q2339466) (← links)
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle (Q2703745) (← links)
• Logical frameworks (Q2751369) (← links)
• Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts (Q2841233) (← links)
• Comparing higher-order encodings in logical frameworks and tile logic (Q2841275) (← links)
• A framework for defining logical frameworks (Q2864157) (← links)
• Realizing the dependently typed \(\lambda\)-calculus (Q2883111) (← links)
• Applicable Mathematics in a Minimal Computational Theory of Sets (Q4553281) (← links)
• Structuring metatheory on inductive definitions (Q4647512) (← links)
• A natural deduction approach to dynamic logic (Q4647578) (← links)
• (Q4849246) (← links)
• Equivalences between logics and their representing type theories (Q4862761) (← links)
• Introduction: Non-classical Logics—Between Semantics and Proof Theory (In Relation to Arnon Avron’s Work) (Q5020161) (← links)
• Logic representation in LF (Q5096264) (← links)
• LF+ in Coq for "fast and loose" reasoning (Q5210657) (← links)
• A practical implementation of simple consequence relations using inductive definitions (Q5234714) (← links)
• A logical framework combining model and proof theory (Q5400853) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• Subtyping dependent types (Q5958760) (← links)
• Investigations into proof-search in a system of first-order dependent function types (Q6488534) (← links)