A sequent calculus with dependent types for classical arithmetic.

Étienne Miquey

Published in: LICS (2018)

Keyphrases

sequent calculus
cut elimination
inference rules
linear logic
pairwise
general purpose
modal logic