PSC 2014 ABSTRACTS: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C E H I J K M N O P R S T

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