A Classical Sequent Calculus with Dependent Types

DOI10.1007/978-3-662-54434-1_29zbMath1485.68071OpenAlexW3128607236MaRDI QIDQ2988668

É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

sequent calculusdependent typesclassical logiccontrol operatorscall-by-valuevalue restrictiondelimited continuationscontinuation-passing-style translation

Mathematics Subject Classification ID

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

Related Items (1)

ANF preserves dependent types up to extensional equality

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A type-theoretic foundation of delimited continuations
• The calculus of constructions
• CPS translations and applications: The cube and beyond
• A symmetric lambda calculus for classical program extraction
• A Classical Realizability Model for a Semantical Value Restriction
• Dependent Types and Fibred Computational Effects
• The duality of computation
• A Categorical Semantics for Linear Logical Frameworks
• Sequent calculus as a compiler intermediate language
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• Existential witness extraction in classical realizability and via a negative translation
• An approach to call-by-name delimited continuations
• Proofs of strong normalisation for second order classical natural deduction
• Hybrid realizability for intuitionistic and classical choice
• Call-by-value is dual to call-by-name
• Functional and Logic Programming
• Typed Lambda Calculi and Applications

This page was built for publication: A Classical Sequent Calculus with Dependent Types