Publication List
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. |
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. |
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).
Embedding a Logical Theory of Constructions in Agda
(abstract,
DOI,
bibtex).
Dependent Types at Work
(abstract,
DOI,
bibtex).
|
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).
|
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. |
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).
|
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. |
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. |