A classical sequent calculus with dependent types

DOI10.1007/978-3-662-54434-1_29MaRDI QIDQ2988668zbMATH OpenOpenAlexFDO

Authors Étienne Miquey

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01375977/file/dL.pdf

zbMATH Keywords

call-by-valueclassical logiccontinuation-passing-style translationcontrol operatorsdelimited continuationsdependent typessequent calculusvalue restriction

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A sequent calculus with dependent types for classical arithmetic
• A type-theoretic foundation of delimited continuations
• A Classical Realizability Model for a Semantical Value Restriction
• Programming and Proving with Classical Types
• Typed Lambda Calculi and Applications

Cites work

• A categorical semantics for linear logical frameworks
• A Classical Realizability Model for a Semantical Value Restriction
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• A symmetric lambda calculus for classical program extraction
• A type-theoretic foundation of delimited continuations
• An approach to call-by-name delimited continuations
• Call-by-value is dual to call-by-name
• CPS translations and applications: The cube and beyond
• Dependent types and fibred computational effects
• Existential witness extraction in classical realizability and via a negative translation
• Functional and Logic Programming
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• Hybrid realizability for intuitionistic and classical choice
• On various negative translations
• Proofs of strong normalisation for second order classical natural deduction
• Sequent calculus as a compiler intermediate language
• The calculus of constructions
• The duality of computation
• Typed Lambda Calculi and Applications

Cited in

(5)

• scientific article; zbMATH DE number 2087549 (Why is no real title available?)
• ANF preserves dependent types up to extensional equality
• A sequent calculus with dependent types for classical arithmetic
• Typed Lambda Calculi and Applications
• A dependent dependency calculus

This page was built for publication: A classical sequent calculus with dependent types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988668)