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


Last modified: Mon Dec 7 18:17:34 CET 2015