Sequent Calculus and Equational Programming

descriptionPublicationkeyboard_double_arrow_right Article , Preprint , Conference object , Other literature type 27 Jul 2015Embargo end date: 01 Jan 2015 English Publisher:Open Publishing AssociationJournal:Electronic Proceedings in Theoretical Computer Science, volume 185, pages 102-109 (eissn: 2075-2180,

Copyright policy )

Authors: Nicolas Guenot; Daniel Gustafsson;

doi: 10.4204/eptcs.185.7 , 10.48550/arxiv.1507.08056

arXiv: 1507.08056

Sequent Calculus and Equational Programming

- Summary
- Subjects
- Metrics

Abstract

Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in equational style. We show here that the equational approach corresponds to the use of a focused presentation of a type theory expressed as a sequent calculus. A typed functional language is presented, based on a sequent calculus, that we relate to the syntax and internal language of Agda. In particular, we discuss the use of patterns and case splittings, as well as rules implementing inductive reasoning and dependent products and sums.

In Proceedings LFMTP 2015, arXiv:1507.07597

Related Organizations

IT University of Copenhagen
Denmark

Keywords

FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Electronic computers. Computer science, QA1-939, QA75.5-76.95, Mathematics, Logic in Computer Science (cs.LO)

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average