Focalisation And Classical Realisability
CSL'09/EACSL'09: Proceedings of the 23rd CSL international conference and 18th EACSL Annual conference on Computer science logic(2009)
摘要
We develop a polarised variant of Curien and Herbelin's (lambda) over bar mu(mu) over tilde calculus suitable for sequent calculi that admit a focalising cut elimination (i.e. whose proofs are focalised when cut-free), such as Girard's classical logic LC or linear logic. This gives a setting in which Krivine's classical realisability extends naturally (in particular to call-by-value), with a presentation in terms of orthogonality. We, give examples of applications to the theory of programming languages.
更多查看译文
关键词
classical logic,classical realisability,linear logic,focalising cut elimination,polarised variant,programming language,sequent calculus
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络