Small proof witnesses for LF

Susmit Sarkar*, Brigitte Pientka, Karl Crary

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationProceedings of 21st International Conference on Logic Programming (ICLP 2005)
PublisherSpringer
Pages387-401
Number of pages15
Volume3668
DOIs
Publication statusPublished - 2005
Event21st International Conference on Logic Programming, ICLP 2005 - Sitges, Spain
Duration: 2 Oct 20055 Oct 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer-Verlag
ISSN (Print)0302-9743

Conference

Conference21st International Conference on Logic Programming, ICLP 2005
Country/TerritorySpain
CitySitges
Period2/10/055/10/05

Fingerprint

Dive into the research topics of 'Small proof witnesses for LF'. Together they form a unique fingerprint.

Cite this