LFSC for SMT proofs: Work in progress

Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley D Eades, Corey Oliver, Ruoyu Zhang

Research output: Contribution to journalConference article

1 Scopus citations

Abstract

This paper presents work in progress on a new version, for public release, of the Logical Framework with Side Conditions (LFSC), previously proposed as a proof meta-format for SMT solvers and other proof-producing systems. The paper reviews the type-theoretic approach of LFSC, presents a new input syntax which hides the type-theoretic details for better accessibility, and discusses work in progress on formalizing and implementing a revised core language.

Original languageEnglish (US)
Pages (from-to)21-27
Number of pages7
JournalCEUR Workshop Proceedings
Volume878
Publication statusPublished - Dec 1 2012
Externally publishedYes
Event2nd International Workshop on Proof Exchange for Theorem Proving, PxTP 2012 - Manchester, United Kingdom
Duration: Jun 30 2012Jun 30 2012

    Fingerprint

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Stump, A., Reynolds, A., Tinelli, C., Laugesen, A., Eades, H. D., Oliver, C., & Zhang, R. (2012). LFSC for SMT proofs: Work in progress. CEUR Workshop Proceedings, 878, 21-27.