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. 1 Implicit Syntax Type theories are powerful formal systems that capture both the notion of computation and deduction. Particularly the expressive theories, such as the Calculus of Constructions (CC) ...

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Marko Luther
• Keywords: Automated Reasoning, CADE 2001, Effective Erasure Methods, Powerful Formal Systems, Such Ambiguous Representations