@inproceedings{Norrish_04, address = {Park City, Utah, United States}, author = {Norrish, Michael}, booktitle = {International Conference on Theorem Proving in Higher Order Logics}, doi = {10.1007/978-3-540-30142-4_18}, editor = {{Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan}}, month = sep, pages = {241---256}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/6610.pdf}, publisher = {Springer}, slides = {https://trustworthy.systems/publications/nicta_slides/6610.pdf}, title = {Recursive Function Definition for Types with Binders}, year = {2004} }