VSL 2014: VIENNA SUMMER OF LOGIC 2014

This page contains an index consisting of author-provided keywords.

B
bi-intuitionistic logic	Dualized Type Theory
C
Call by name	A type system for Continuation Calculus
Call by value	A type system for Continuation Calculus
call-by-name and call-by-value	Confluence for classical logic through the distinction between values and computations
CERES	Cut-Elimination in Schematic Proofs and Herbrand Sequents
classical logic	Dualized Type Theory Infinitary Classical Logic: Recursive Equations and Interactive Semantics
Classical realizability	Dualized Type Theory
Combinatorial proofs	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
completeness	Dualized Type Theory Extensional Models of Typed Lambda-mu Calculus
computational content	A sheaf model of the algebraic closure
Consistency	Dualized Type Theory
constructive algebra	A sheaf model of the algebraic closure
context semantics	Stratified Nested Linear Logic
continuations	A type system for Continuation Calculus
cps translation	Confluence for classical logic through the distinction between values and computations
cut elimination	Cut-Elimination in Schematic Proofs and Herbrand Sequents
cut-elimination	Confluence for classical logic through the distinction between values and computations
D
duality	Dualized Type Theory
E
extensional models	Extensional Models of Typed Lambda-mu Calculus
F
First-order classical proof nets	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
First-order Classical Sequent Calculus	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
G
Game Semantics	Infinitary Classical Logic: Recursive Equations and Interactive Semantics
Gentzen's sharpened Hauptsatz	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
H
Henkin Quantifier	Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions'
Herbrand Sequent	Cut-Elimination in Schematic Proofs and Herbrand Sequents
Herbrand's theorem	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
Heyting Algebra Expansions	Negative Translations and Heyting Algebra Expansions
Heyting Arithmetic	A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
I
implicit computational complexity	Stratified Nested Linear Logic
Induction	Cut-Elimination in Schematic Proofs and Herbrand Sequents
Infinitary Trees	Infinitary Classical Logic: Recursive Equations and Interactive Semantics
Intersection and union types	A Translation of Intersection and Union Types for the lambda-mu Calculus
intuitionistic modal logic	Negative Translations and Heyting Algebra Expansions
intuitionistic-modal Kripke frames	Negative Translations and Heyting Algebra Expansions
K
kripke model	Dualized Type Theory
L
lambda calculus	A type system for Continuation Calculus
lambda-mu calculus	A Translation of Intersection and Union Types for the lambda-mu Calculus Extensional Models of Typed Lambda-mu Calculus
light logics	Stratified Nested Linear Logic
linear logic	Stratified Nested Linear Logic A proof-theoretic view on scheduling in concurrency
Ludics	Infinitary Classical Logic: Recursive Equations and Interactive Semantics
M
Markov's Principle	A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
Midsequent theorem	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
monadic language	Confluence for classical logic through the distinction between values and computations
N
Negative translation	A Translation of Intersection and Union Types for the lambda-mu Calculus
negative translations	Negative Translations and Heyting Algebra Expansions
non-determinism	A proof-theoretic view on scheduling in concurrency
non-extensional computation	Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions'
P
polynomial time	Stratified Nested Linear Logic
process calculus	A proof-theoretic view on scheduling in concurrency
proof theory	A proof-theoretic view on scheduling in concurrency
R
realizability	A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
Recursive Types	Infinitary Classical Logic: Recursive Equations and Interactive Semantics
resolution	Cut-Elimination in Schematic Proofs and Herbrand Sequents
Rule transposition	Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
S
scheduling	A proof-theoretic view on scheduling in concurrency
Schematic Proof	Cut-Elimination in Schematic Proofs and Herbrand Sequents
Scott data types	A type system for Continuation Calculus
semantics	A proof-theoretic view on scheduling in concurrency
sequent calculus	Dualized Type Theory Confluence for classical logic through the distinction between values and computations
sheaf model	A sheaf model of the algebraic closure
simply-typed lambda-calculus	Confluence for classical logic through the distinction between values and computations
Strong normalisation	A Translation of Intersection and Union Types for the lambda-mu Calculus
T
type preservation	Dualized Type Theory
type system	Extensional Models of Typed Lambda-mu Calculus
types	A type system for Continuation Calculus
U
uniform continuity	Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions'
W
weak normalization	Dualized Type Theory

Disclaimer | Powered by EasyChair Smart Program