Pages that link to "Item:Q688571"
From MaRDI portal
The following pages link to Using typed lambda calculus to implement formal systems on a machine (Q688571):
Displaying 21 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)
- Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. (Q2841233) (← links)
- Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic (Q2841275) (← links)
- A Framework for Defining Logical Frameworks (Q2864157) (← links)
- Logic representation in LF (Q5096264) (← links)
- LF+ in Coq for "fast and loose" reasoning (Q5210657) (← links)
