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 Citation (Scopus)

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

Surface mount technology

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.

LFSC for SMT proofs : Work in progress. / Stump, Aaron; Reynolds, Andrew; Tinelli, Cesare; Laugesen, Austin; Eades, Harley D; Oliver, Corey; Zhang, Ruoyu.

In: CEUR Workshop Proceedings, Vol. 878, 01.12.2012, p. 21-27.

Research output: Contribution to journalConference article

Stump, A, Reynolds, A, Tinelli, C, Laugesen, A, Eades, HD, Oliver, C & Zhang, R 2012, 'LFSC for SMT proofs: Work in progress', CEUR Workshop Proceedings, vol. 878, pp. 21-27.
Stump A, Reynolds A, Tinelli C, Laugesen A, Eades HD, Oliver C et al. LFSC for SMT proofs: Work in progress. CEUR Workshop Proceedings. 2012 Dec 1;878:21-27.
Stump, Aaron ; Reynolds, Andrew ; Tinelli, Cesare ; Laugesen, Austin ; Eades, Harley D ; Oliver, Corey ; Zhang, Ruoyu. / LFSC for SMT proofs : Work in progress. In: CEUR Workshop Proceedings. 2012 ; Vol. 878. pp. 21-27.
@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 Eades, {Harley D} and Corey Oliver and Ruoyu Zhang",
year = "2012",
month = "12",
day = "1",
language = "English (US)",
volume = "878",
pages = "21--27",
journal = "CEUR Workshop Proceedings",
issn = "1613-0073",
publisher = "CEUR-WS",

}

TY - JOUR

T1 - LFSC for SMT proofs

T2 - Work in progress

AU - Stump, Aaron

AU - Reynolds, Andrew

AU - Tinelli, Cesare

AU - Laugesen, Austin

AU - Eades, Harley D

AU - Oliver, Corey

AU - Zhang, Ruoyu

PY - 2012/12/1

Y1 - 2012/12/1

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

VL - 878

SP - 21

EP - 27

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

SN - 1613-0073

ER -