Open AccessA Classical Sequent Calculus with Dependent Types
Author(s) -
Étienne Miquey
Publication year - 2019
Publication title -
acm transactions on programming languages and systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.233
H-Index - 70
eISSN - 1558-4593
pISSN - 0164-0925
DOI - 10.1145/3230625
Subject(s) - sequent calculus , soundness , sequent , natural deduction , cut elimination theorem , mathematical proof , calculus (dental) , computer science , curry–howard correspondence , continuation , mathematics , algebra over a field , programming language , pure mathematics , medicine , geometry , dentistry
Dependent types are a key feature of the proof assistants based on the Curry-Howard isomorphism. It is well known that this correspondence can be extended to classical logic by enriching the langua...
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom