# Bibtex References

@TechReport{bove/arbilla:tr91, author = {A. Bove and L. Arbilla}, title = {A Confluent Calculus of Macro Expansion and Evaluation}, institution = {Instituto de Computaci\'on, Facultad de Ingenier\'{i}a, Universidad de la Rep\'ublica, Uruguay}, year = {1991}, number = {INCO-91-01}, month = {December} }

@InProceedings{bove/arbilla:lfp92, author = {A. Bove and L. Arbilla}, title = {A confluent calculus of Macro expansion and evaluation}, booktitle = {Proceedings of the 1992 ACM conference on LISP and Functional Programming, San Francisco, California, USA}, pages = {278--287}, year = {1992}, month = {June}, publisher = {ACM Press} }

@MastersThesis{bove:master, author = {A. Bove}, title = {A Machine-Assisted Proof of the Subject Reduction Property for a Small Typed Functional Language}, school = {Department of Computer Science, Universidad de la Repl\'ublica}, year = {1995}, address = {Uruguay}, month = {November}, note = {Technical Report INCO-95-06}, annote = {Technical Report INCO-95-06 ISSN 0797-6410} }

@TechReport{bove:wtecngw, author = {A. Bove}, title = {A Machine-Assisted Proof that Well Typed Expressions Cannot Go Wrong}, institution = {Department of Computing Science, Chalmers University of Technology}, year = {1998}, address = {G\"oteborg, Sweden}, OPTmonth = {May} }

@InProceedings{bove/severi:alpha_conversion, author = {A. Bove and P. Severi}, title = {Alpha Conversion in Simply Typed Lambda Calcul}, booktitle = {Workshop on Logic, Language, Information and Computation, WOLLIC'99}, year = {1999}, month = {May} }

@Misc{bove:lic, author = {A. Bove}, title = {Programming in {M}artin-{L}\"of Type Theory: {U}nification - {A} non-trivial Example}, year = {1999}, month = {November}, note = {Licentiate Thesis of the Department of Computer Science, Chalmers University of Technology} }

@Article{bove:njc, author = {A. Bove}, title = {Simple General Recursion in Type Theory}, journal = {Nordic Journal of Computing}, year = {2001}, volume = {8}, number = {1}, pages = {22--42} }

@InProceedings{bove/capretta:nested_rec, author = {A. Bove and V. Capretta}, title = {Nested General Recursion and Partiality in Type Theory}, booktitle = {Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001}, pages = {121--135}, year = {2001}, editor = {R. J. Boulton and P. B. Jackson}, series = {LNCS 2152}, month = {September} }

@unpublished{bove:mutual_rec, author = {A. Bove}, title = {Mutual General Recursion in Type Theory}, year = {2002}, month = {May}, note = {Technical Report, Department of Computing Science, Chalmers University of Technology} }

@unpublished{bove:gen_sim_ind_rec, author = {A. Bove}, title = {Generalised Simultaneous Inductive-Recursive Definitions and their Applications to Programming in Type Theory}, year = {2002}, month = {September}, note = {Technical Report, Department of Computing Science, Chalmers University of Technology} }

@PhdThesis{bove:phd_thesis, author = {A. Bove}, title = {General Recursion in Type Theory}, school = {Department of Computing Science, Chalmers University of Technology}, year = {2002}, month = {November} }

@InProceedings{bove:tutorial, author = {A. Bove}, title = {General Recursion in Type Theory}, booktitle = {Types for Proofs and Programs, International Workshop TYPES 2002, The Netherlands}, pages = {39--58}, year = 2002, editor = {H. Geuvers and F. Wiedijk}, series = {LNCS 2646}, month = {April} }

@Misc{bove:bitonic, author = {A. Bove}, title = {Formalising Bitonic Sort using Dependent Types}, note = {Technical Report, Chalmers University of Technology}, month = {October}, year = {2004} }

@InProceedings{bove/coquand:bitonic, author = {A. Bove and T. Coquand}, title = {Formalising Bitonic Sort in Type Theory}, booktitle = {Types for Proofs and Programs International Workshop, TYPES 2004, France}, pages = {82--97}, year = {2004}, editor = {J-C.~Filliatre, C.~Paulin-Mohring and B.~Werner}, series = {LNCS 3839}, month = {December} }

@Article{bove/capretta:general_rec, author = {A. Bove and V. Capretta}, title = {Modelling General Recursion in Type Theory}, journal = {Mathematical Structures in Computer Science}, year = {2005}, month = {February}, volume = {15}, pages = {671--708}, note = {Cambridge University Press} }

@InProceedings{bove/capretta:hof, author = {A. Bove and V. Capretta}, title = {Recursive Functions with Higher Order Domains}, booktitle = {Typed Lambda Calculi and Applications TLCA'05}, pages = {115--130}, year = 2005, series = {LNCS 3461}, month = {April}, publisher = {Springer} }

@InProceedings{abel:monadic_translation, author = {A. Abel and M. Benke and A. Bove and J. Hughes and U. Norell}, title = {Verifying {H}askell Programs using Constructive Type Theory}, booktitle = {Haskell Workshop}, month = {September}, year = 2005, publisher = {ACM} }

@InProceedings{bove/capretta:prophecy, author = {A. Bove and V. Capretta}, title = {Computation by Prophecy}, booktitle = {Typed Lambda Calculi and Applications TLCA'07}, pages = {70--83}, year = {2007}, series = {LNCS 4583}, month = {June} }

@InProceedings{bove/capretta:type-prf, author = {A. Bove and V. Capretta}, title = {A Type of Partial Recursive Functions}, booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, pages = {102--117}, year = {2008}, editor = {O. Mohamed and C. Mu\~noz and A. Tahar}, volume = {5170}, series = {LNCS}, month = {August}, publisher = {Springer} }

@Book{bove:lernet2008, editor = {A. Bove and L. Barbosa and A. Pardo and J. Sousa Pinto}, title = {Language Engineering and Rigorous Software Development}, publisher = {Springer}, year = {2009}, volume = {5520}, series = {LNCS}, note = {International LerNet ALFA Summer School, Piri\'apolis, Uruguay, February 24 - March 1, 2008. Revised, Selected Papers.} }

@InProceedings{bove/dybjer:dep_types, author = {A. Bove and P. Dybjer}, title = {Dependent Types at Work}, booktitle = {Language Engineering and Rigorous Software Development International LerNet ALFA Summer School}, pages = {57--99}, year = {2009}, editor = {A. Bove and L. Barbosa and A. Pardo and J. Sousa Pinto}, volume = {5520}, series = {LNCS}, publisher = {Springer}, }

@InProceedings{bove/dybjer/sicard:ltc, author = {A. Bove and P. Dybjer and A. Sicard-Ram\'{i}rez}, title = {Embedding a Logical Theory of Constructions in Agda}, booktitle = {Programming Languages meets Program Verification (PLPV) 2009}, year = {2009}, series = {ACM digital library}, month = {January}, }

@InProceedings{bove:dom_graphs, author = {A. Bove}, title = {Another Look at Function Domains}, booktitle = {Mathematical Foundations of Programme Semantics, 25th Annual Conference}, pages = {61--74}, year = {2009}, editor = {S. Abramsky and M. Mislove and C. Palamidessi}, volume = {249C}, series = {ENTCS}, month = {April}, }

@InProceedings{bove/dybjer/norel:agda_tutorial, author = {A. Bove, P. Dybjer, and U. Norell}, title = {A Brief Overview of Agda - A Functional Language with Dependent Types}, booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009}, pages = {73--78}, year = {2009}, editor = {S. Berghofer and T. Nipkow and C. Urban and M. Wenzel}, volume = {5674}, series = {LNCS}, month = {August}, publisher = {Springer}, }

@Proceedings{bove:par2010, title = {Proceedings of Workshop on Partiality and Recursion in Interactive Theorem Provers}, year = {2010}, editor = {A. Bove, E. Komendantskaya and M. Niqui}, volume = {43}, series = {EPTCS}, month = {July}, }

@InProceedings{bove/dybjer/sicard:fossacs2012, author = {A. Bove and P. Dybjer and A. Sicard-Ram\'{i}rez}, title = {Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs}, booktitle = {15th International Conference on {F}oundations of {S}oftware {S}cience and {C}omputational {S}tructures, {FoSSaCS} 2012}, pages = {104--118}, year = {2012}, editor = {Lars Birkedal}, volume = {7213}, series = {LNCS}, month = {March} }

@Article{bove/krauss/sozeau:partiality, author = {A. Bove and A. Krauss and M. Sozeau}, title = {Partiality and Recursion in Interactive Theorem Provers --- An Overview}, journal = {Mathematical Structures in Computer Science}, year = {2016}, volume = {26}, pages = {38--88}, month = {January}, note = {Published online: November 2014} }