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 30 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)
- 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)
- 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)
