An insider's look at LF type reconstruction: everything you (n)ever wanted to know
From MaRDI portal
Publication:4912883
Recommendations
Cites work
- A Linear Spine Calculus
- A framework for defining logics
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Logic, language and computation. Festschrift in Honor of Satoru Takasu
- Mechanizing metatheory in a logical framework
- The view from the left
Cited in
(7)- Proof-relevant Horn clauses for dependent type inference and term synthesis
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- A case study in programming coinductive proofs: Howe's method
- Inductive beluga: programming proofs
- Type Reconstruction for General Refinement Types
- Mechanizing proofs with logical relations -- Kripke-style
- Harpoon: mechanizing metatheory interactively
This page was built for publication: An insider's look at LF type reconstruction: everything you (n)ever wanted to know
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4912883)