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}
}