LFSC for SMT proofs: Work in progress

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

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 journal › Conference article › peer-review

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 language	English (US)
Pages (from-to)	21-27
Number of pages	7
Journal	CEUR Workshop Proceedings
Volume	878
State	Published - 2012
Externally published	Yes
Event	2nd International Workshop on Proof Exchange for Theorem Proving, PxTP 2012 - Manchester, United Kingdom Duration: Jun 30 2012 → Jun 30 2012

ASJC Scopus subject areas

Computer Science(all)

Cite this

@article{4a256992508b454c80e391f82b70f37c,

title = "LFSC for SMT proofs: Work in progress",

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.",

author = "Aaron Stump and Andrew Reynolds and Cesare Tinelli and Austin Laugesen and Harley Eades and Corey Oliver and Ruoyu Zhang",

year = "2012",

language = "English (US)",

volume = "878",

pages = "21--27",

journal = "CEUR Workshop Proceedings",

issn = "1613-0073",

publisher = "CEUR-WS",

note = "2nd International Workshop on Proof Exchange for Theorem Proving, PxTP 2012 ; Conference date: 30-06-2012 Through 30-06-2012",

}

TY - JOUR

T1 - LFSC for SMT proofs

T2 - 2nd International Workshop on Proof Exchange for Theorem Proving, PxTP 2012

AU - Stump, Aaron

AU - Reynolds, Andrew

AU - Tinelli, Cesare

AU - Laugesen, Austin

AU - Eades, Harley

AU - Oliver, Corey

AU - Zhang, Ruoyu

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84891911241&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84891911241&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:84891911241

SN - 1613-0073

VL - 878

SP - 21

EP - 27

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

Y2 - 30 June 2012 through 30 June 2012

ER -

LFSC for SMT proofs: Work in progress

Abstract

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this