LFSC for SMT proofs: Work in progress

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

Research output: Contribution to journalConference articlepeer-review

2 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
StatePublished - 2012
Externally publishedYes
Event2nd International Workshop on Proof Exchange for Theorem Proving, PxTP 2012 - Manchester, United Kingdom
Duration: Jun 30 2012Jun 30 2012

ASJC Scopus subject areas

  • General Computer Science

Fingerprint

Dive into the research topics of 'LFSC for SMT proofs: Work in progress'. Together they form a unique fingerprint.

Cite this