More On Implicit Syntax

Proof assistants based on type theories, such as Coq and LEGO, allow users to omit subterms on input that can be inferred automatically. While those mechanisms are well known, ad-hoc algorithms are used to suppress subterms on output. As a result, terms might be printed identically although they differ in hidden parts. Such ambiguous representations may confuse users. Additionally, terms might be rejected by the type checker because the printer has erased too much type information. This paper addresses these problems by proposing effective erasure methods that guarantee successful term reconstruction, similar to the ones developed for the compression of proof-terms in Proof-Carrying Code environments. Experiences with the implementation in Typelab proved them both efficient and practical.
 

Online Copy

Available as PDF (15 pages, ca 228 KB)
 

BibTeX Entry

@inProceedings{luther:01a,
   crossref = {IJCAR:01},
   author =   {Luther, Marko},
   title =    {More On Implicit Syntax},
   year =     2001,
   pages =    {386--400},
   url =      {ftp://ftp.informatik.uni-ulm.de/pub/KI/papers/ijcar01.pdf},
}

@proceedings{IJCAR:01,
   editors =   {Gor{\'{e}}, R. and Leitsch, A. and Nipkow, T.},
   booktitle = {Automated Reasoning. First International Joint Conference 
                ({IJCAR}'01), Siena, Italy, June 18--23, 2001, Proceedings},
   series =    {Lecture Notes in Artificial Intelligence},
   publisher = {Springer-Verlag},
   volume =    2083,
   address =   {Berlin},
   year =      2001,
}