Sciweavers

ICLP
2005
Springer

Small Proof Witnesses for LF

13 years 9 months ago
Small Proof Witnesses for LF
Abstract. We instrument a higher-order logic programming search procedure to generate and check small proof witnesses for the Twelf system, an implementation of the logical framework LF. In particular, we extend and generalize ideas from Necula and Rahul [16] in two main ways: 1) We consider the full fragment of LF including dependent types and higher-order terms and 2) We study the use of caching of sub-proofs to further compact proof representations. Our experimental results demonstrate that many of the restrictions in previous work can be overcome and generating and checking small witnesses within Twelf provides valuable addition to its general safety infrastructure.
Susmit Sarkar, Brigitte Pientka, Karl Crary
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where ICLP
Authors Susmit Sarkar, Brigitte Pientka, Karl Crary
Comments (0)