A project on this topic would suit someone with an interest in category theory, in dependent type theory and in the use of proof assistants based upon dependent type theory for formalizing mathematics.
M. Hofmann, "Syntax and semantics of dependent types". In A. Pitts and P. Dybjer, editors, Semantics and Logics of Computation (Cambridge University Press, 1996).
The paperA. Abel, T. Coquand and P. Dybjer, "On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory", FLOPS 2008: 3-13.
considers CwFs with Pi-types and a universe. It presents some Haskell code for constructing type-checked normal forms and claims that this gives the initial CwF with Pi-types and a universe. However the claim is not established in the paper. In other words, their type-checking algorithm is not proved to be correct. The purpose of this project would be to explore the use Agda to formalize the theory of CwFs and then attempt to construct an initial CwF with Pi-types and a universe along the lines suggested by Abel-Coquand-Dybjer, together with a proof of correctness.
A project on this topic would suit someone with an interest in typed λ-calculus, in the use of proof assistants based upon dependent type theory for formalizing programming language semantics, and in the theory of nominal sets.
A. M. Pitts, "Structural Recursion with Locally Scoped Names", Journal of Functional Programming, 21(3): 235-286, 2011.
and is a vehicle for exhibiting a new recursion principle for inductively defined data modulo α-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. Remark 3.20 (p261) of that paper says:"The various lemmas and propositions in this section and Appendix C give the proof of Theorem 3.16 [the Normalization Theorem for λαν-calculus] in enough detail to convince the reader of its truth, one hopes. Nevertheless, the nature of what the theorem asserts depends very delicately upon the particular definitions in Figures 5-8. Mistakes in, or changes to (cf. Remark 3.13), those definitions could easily invalidate either the theorem, or some details of our proof of it, in a way that might well be hard to spot without checking all the details that are elided here. Furthermore, in the next section, we extend the λαν-calculus with a form of structural recursion and will have to replay the proof of normalization for this extended calculus [the λανδ-calculus]. For all these reasons, it would be very desirable to have a fully formalized and machine-checked proof of the results in this section in a form that is amenable to extensions."
The purpose of the project would be to develop a fully formalized proof of the normalization theorem for the λανδ-calculus (Theorem 4.7) within the Agda proof assistant, along the lines of the proof for simply typed lambda calculus given inChantal Keller and Thorsten Altenkirch, "Normalization by hereditary substitutions", proceedings of Mathematical Structured Functional Programming (MSFP) 2010
As well as formalizing the proof of Theorems 4.7, which only deals with β-conversion, the project could consider proving similar results for a suitable notion of η-long β-normal form - these would be new results, rather than formalizations of existing results.