VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
Agda	Some constructions on ω-groupoids
alpha equality	A Generic Approach to Proofs about Substitution
C
category theory	Some constructions on ω-groupoids
context	Variable Arity for LF
context free grammars	A Generic Approach to Proofs about Substitution
context schemas	Automatically Deriving Schematic Theorems for Dynamic Contexts
Coq	A Generic Approach to Proofs about Substitution
D
dependent types	A Generic Approach to Proofs about Substitution
dynamic contexts	Automatically Deriving Schematic Theorems for Dynamic Contexts
E
equivariance	A Generic Approach to Proofs about Substitution
F
Formal Metatheory	Gentle Formalisation of Stoughton’s Lambda Calculus Substitution
Formalisation	Some constructions on ω-groupoids
foundations	Proof-Theoretic Foundations of Indexing in Logic Programming
G
generic programming	A Generic Approach to Proofs about Substitution
H
Higher dimensional structures	Some constructions on ω-groupoids
HOAS	Internal Adequacy of Bookkeeping in Coq
homotopy type theory	Some constructions on ω-groupoids
Hybrid Logics	Hybrid Extensions in a Logical Framework
I
indexing	Proof-Theoretic Foundations of Indexing in Logic Programming
L
lambda calculus	Gentle Formalisation of Stoughton’s Lambda Calculus Substitution
LF	A Framework for Implementing Logical Frameworks
logic programming	Proof-Theoretic Foundations of Indexing in Logic Programming
Logical Framework	Hybrid Extensions in a Logical Framework A Framework for Implementing Logical Frameworks
Logical Frameworks	Internal Adequacy of Bookkeeping in Coq
M
MMT	A Framework for Implementing Logical Frameworks
Modal logics	Hybrid Extensions in a Logical Framework
P
polymorphism	A Framework for Implementing Logical Frameworks
poplmark	Variable Arity for LF
proof assistants	Automatically Deriving Schematic Theorems for Dynamic Contexts
proof-theory	Proof-Theoretic Foundations of Indexing in Logic Programming
R
reasoning about contexts	Automatically Deriving Schematic Theorems for Dynamic Contexts
reflection	Automatically Deriving Schematic Theorems for Dynamic Contexts
Rewriting	A Framework for Implementing Logical Frameworks
S
substitution	Gentle Formalisation of Stoughton’s Lambda Calculus Substitution A Generic Approach to Proofs about Substitution
T
tactics and tacticals	Automatically Deriving Schematic Theorems for Dynamic Contexts
tuple	Variable Arity for LF
type theory	Internal Adequacy of Bookkeeping in Coq Some constructions on ω-groupoids
V
variable bindings	A Generic Approach to Proofs about Substitution

Disclaimer | Powered by EasyChair Smart Program