# Questions - Why not Chruch encodings? How to add new types without changing the language implementation? - Motives? - Connor McBride "Elimination with a Motive" - proof refinement (proof by refinement / refinement proofs) https://iohk.io/blog/proof-refinement-basics/ - http://www.cs.cornell.edu/courses/cs4860/2012fa/lec-04.pdf - In/Out typed terms - Pierce and Turner "Local Type inferrence" - http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf - "Input" typed terms - the type can be Inferred (e.g. directly annotated term or type otherwise immediately available). - In-terms can ben used where type inference is needed. - "Out" typed terms - the type can be checked