Publication List

[ Books and Proceedings | Journal Publications | Articles in Proceedings | Technical Reports | Theses ]

See also my official publication list at Chalmers, ordered by year.


Books and Proceedings

2010

Proceedings of the PAR-2010 workshop on Partiality and Recusion in Iteractive Theorem Provers, Edinburgh, Scotland, 15th of July 2010 (DOI, bibtex).
A. Bove, E. Komendantskaya and M. Niqui, editors.
EPTCS volume 43.

2009

Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, Piriápolis, Uruguay, February 24 - March 1, 2008. Revised, selected papers (DOI, bibtex).
A. Bove, L. Barbosa, A. Pardo, and J. Sousa Pinto, editors.
LNCS 5520, 2009.
[top]

Journal Publications

2014

Partiality and Recursion in Interactive Theorem Provers --- An Overview (abstract, DOI, bibtex).
A. Bove, A. Krauss, and M. Sozeau.
In Mathematical Structures in Computer Science, Special Issue 1 (DTP 2010), January 2016, volume 26, pages 38--88.
Published online: November 2014

2005

Modelling General Recursion in Type Theory (abstract, DOI, bibtex).
A. Bove and V. Capretta.
In Mathematical Structures in Computer Science, February 2005, volume 15, pages 671--708.

2001

Simple General Recursion in Type Theory (abstract, bibtex).
Nordic Journal of Computing, volume 8, number 1, Spring 2001.
[top]

Articles in Proceedings

2015

Principles of Alpha-Induction and Recursion for the Lambda Calculus in Constructive Type Theory (abstract).
E. Copello, A. Tasistro, N Szasz, A. Bove and M. Fernández.
In pre-proceedings of LSFA 2015, September 2015.

2012

Combining Interactive and Automatic Reasoning about Functional Programs (abstract, DOI, bibtex).
A. Bove, P. Dybjer and A. Sicard-Ramírez.
In proceedings of FoSSaCS 2012, March 2012, LNCS 7213.

2009

A Brief Overview of Agda - A Functional Language with Dependent Types (abstract, DOI, bibtex).
A. Bove, P. Dybjer, and U. Norell.
Invited tutorial at Theorem Proving in Higher Order Logics 2009.
In proceedings TPHOLs 22nd International Conference, August 2009, LNCS 5674, pages 73--78.

Another Look at Function Domains (abstract, DOI, bibtex).
Invited talk in the special session on Mathematically Structured Functional Programming.
In proceedings of MFPS 25, April 2009, ENTCS 249C, pages 61--74.

Embedding a Logical Theory of Constructions in Agda (abstract, DOI, bibtex).
A. Bove, P. Dybjer and A. Sicard-Ramírez.
In proceedings of PLPV 2009, January 2009, ACM digital library.

Dependent Types at Work (abstract, DOI, bibtex).
A. Bove and P. Dybjer.
Lecture notes for a graduate course on dependent types at the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, Piriápolis, Uruguay, February 2008, LNCS 5520, pages 57--99, 2009.

2008

A Type of Partial Recursive Functions (abstract, DOI, bibtex).
A. Bove and V. Capretta.
In proceedings of TPHOLs 2008, August 2008, LNCS 5170, pages 102--117.

2007

Computation by Prophecy (abstract, DOI, bibtex).
A. Bove and V. Capretta.
In proceedings of TLCA 2007, June 2007, LNCS 4583, pages 70--83.

2005

Verifying Haskell Programs Using Constructive Type Theory (abstract, DOI, bibtex).
A. Abel, M. Benke, A. Bove, J. Hughes and U. Norell.
In proceedings of Haskell Workshop, September 2005, ACM.

Recursive Functions with Higher Order Domains (abstract, DOI, bibtex).
A. Bove and V. Capretta.
In proceedings of TLCA 2005, April 2005, LNCS 3461, pages 115--130.

2004

Formalising Bitonic Sort in Type Theory (abstract, DOI, bibtex).
A. Bove and T. Coquand.
In post workshop proceedings of TYPES 2004, December 2004, LNCS 3839, pages 82--97.

2002

General Recursion in Type Theory (abstract, DOI, bibtex).
Tutorial paper on the method for defining general recursive algorithms in type theory.
In post workshop proceedings of TYPES 2002, LNCS 2646, held in Berg en Dal, The Netherlands, April 2002.

2001

Nested General Recursion and Partiality in Type Theory (abstract, DOI, bibtex).
A. Bove and V. Capretta.
In proceedings of TPHOLs'01, LNCS 2152, held in Edinburgh, Scotland, September 2001.

1999

Alpha Conversion in Simply Typed Lambda Calculus (abstract, pdf, bibtex).
A. Bove and P. Severi.
In proceedings of the WOLLIC'99, Rio de Janeiro, Brazil, May 1999.

1992

A Confluent Calculus of Macro Expansion and Evaluation (abstract, DOI, bookmark, bibtex).
A. Bove and L. Arbilla.
In the proceedings of Lisp and Functional Programming '92 (LFP'92), San Francisco, California, USA, June 1992.
[top]

Technical Reports

2004

Formalising Bitonic Sort using Dependent Types (abstract, pdf, bibtex).
Technical report, Department of Computer Science and Engineering, Chalmers. October 2004.

2002

Generalised Simultaneous Inductive-Recursive Definitions and their Application to Programming in Type Theory (abstract, pdf, bibtex).
Similar to the paper below. It has a better introduction for those not familiar with the method for formalising general recursion in type theory. The paper below jumps directly into the problem of how to formalise mutual recursion in type theory.
Technical report, Department of Computing Science, Chalmers, September 2002.

Mutual General Recursion in Type Theory (abstract, pdf, bibtex).
Technical report, Department of Computing Science, Chalmers, May 2002.

1998

A Machine-assisted Proof that Well Typed Expressions Cannot Go Wrong (abstract, pdf, bibtex, pdf of shorter version).
Technical report, Department of Computing Science, Chalmers, May 1998.

1991

A Confluent Calculus of Macro Expansion and Evaluation (abstract, pdf, bibtex).
A. Bove and L. Arbilla.
Technical Report of the InCo, December 1991. Complete version of the paper presented at LFP'92.

1990

Diseño e Implementación de un Intérprete para el Lenguaje Funcional TLL (Design and Implementation of an Interpreter for the Language TLL (Typed Lambda Language)).
A. Bove and Andrómaca Tasistro.
Technical Report of the ESLAI, August 1990.
[top]

Theses

2002

General Recursion in Type Theory (abstract, pdf, bibtex).
PhD Thesis, Department of Computing Science, Chalmers, November 2002.

1999

Programming in Martin-Löf Type Theory: Unification - A non-trivial Example (abstract, pdf, bibtex).
Licentiate Thesis, Department of Computing Science, Chalmers, November 1999.

1995

A Machine-assisted Proof of the Subject Reduction Property for a Small Typed Functional Language (abstract, pdf, bibtex).
Master thesis and Technical report of the InCo, Uruguay, November 1995.
Together with Alvaro Tasistro, we published an extended abstract (pdf in proceedings of the WOLLIC'96, May 1996).

1990

Una Semántica de Abreviaciones Sintácticas usando Sustituciones Explícitas (A Semantics of Syntactic Abbreviations using Explicit Substitutions).
Bachelor's thesis and Technical Report of the ESLAI (Latin-American High School of Computer Science), December 1990.
[top]