VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
Ancestral logic	Intuitionistic Ancestral Logic
B
Bar recursion	Effective Bounds on the Podelski-Rybalchenko Termination Theorem
Behavioural Differential Equations	Observational Equivalence for Behavioural Differential Equations
BHK interpretation	A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic
C
call-by-name	A typed lambda-calculus with call-by-name and call-by-value iteration
call-by-value	A typed lambda-calculus with call-by-name and call-by-value iteration
Church's type theory	Program extraction in Church's simple theory of types (invited talk)
Coinductive Types	Observational Equivalence for Behavioural Differential Equations
Completeness theorem for classical logic	Computing with Gödel’s completeness theorem
Completeness theorems	Constructive completeness and exploding models
computational content	Computing with Gödel’s completeness theorem
Constructive type theory	Intuitionistic Ancestral Logic
continuation	A typed lambda-calculus with call-by-name and call-by-value iteration
E
Extraction	Extracting Monadic Parsers from Proofs
H
Henkin's proof	Computing with Gödel’s completeness theorem
higher-order logic	Program extraction in Church's simple theory of types (invited talk)
I
Intuitionism	Effective Bounds on the Podelski-Rybalchenko Termination Theorem
intuitionistic logic	Computing with Gödel’s completeness theorem Intuitionistic Ancestral Logic A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic
intuitionistic propositional logic	Proof-search in natural deduction calculi for IPL
intuitionistic set theory	Constructive completeness and exploding models
iteration	A typed lambda-calculus with call-by-name and call-by-value iteration
J
Justification Logic	Multi-agent justification logic
K
Kripke semantics	Constructive completeness and exploding models
M
Minlog	Extracting Monadic Parsers from Proofs
modal logic	Multi-agent justification logic
Monad	Extracting Monadic Parsers from Proofs
Monotone induction and coinduction	Program extraction in Church's simple theory of types (invited talk)
N
natural deduction	Proof-search in natural deduction calculi for IPL
O
Observational Equivalence	Observational Equivalence for Behavioural Differential Equations
Observational Type Theory	Observational Equivalence for Behavioural Differential Equations
P
Parser	Extracting Monadic Parsers from Proofs
Program extraction	Program extraction in Church's simple theory of types (invited talk)
proof-search	Proof-search in natural deduction calculi for IPL
R
Ramsey Theorem	Effective Bounds on the Podelski-Rybalchenko Termination Theorem
realizability	Program extraction in Church's simple theory of types (invited talk)
Realizability semantics	Intuitionistic Ancestral Logic
realization	Multi-agent justification logic
S
Scott data types	A typed lambda-calculus with call-by-name and call-by-value iteration
Set-theory	Extracting Monadic Parsers from Proofs
sheaf	A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic
strong normalization	A typed lambda-calculus with call-by-name and call-by-value iteration
T
termination	Extracting Monadic Parsers from Proofs
Termination Theorem	Effective Bounds on the Podelski-Rybalchenko Termination Theorem
Transitive closure	Intuitionistic Ancestral Logic
Typed lambda calculus	A typed lambda-calculus with call-by-name and call-by-value iteration

Disclaimer | Powered by EasyChair Smart Program