CADE-28: THE 28TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

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

A
Automated Deduction	Automating Induction by Reflection
Automated Induction	Automating Induction by Reflection
automated reasoning	Automating Induction by Reflection
Axiomatic Theories of Truth	Automating Induction by Reflection
B
bana-comon	Foundations of the Squirrel meta-logic for reasoning over security protocols
C
Case Analysis	Adelfa: A System for Reasoning about LF Specifications
ccsa	Foundations of the Squirrel meta-logic for reasoning over security protocols
computational model	Foundations of the Squirrel meta-logic for reasoning over security protocols
contexts	Interacting safely with an unsafe environment
Coq	SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts Countability of Inductive Types Formalized in the Object-Logic Level The MetaCoq Project
countable	Countability of Inductive Types Formalized in the Object-Logic Level
D
Datalog	Towards a Semantic Framework for Policy Exchange in the Internet
dependent type	Countability of Inductive Types Formalized in the Object-Logic Level
DSL	A logical framework with a graph meta-language
E
Edinburgh Logical Framework	Adelfa: A System for Reasoning about LF Specifications
F
Facilitating	Facilitating Meta-Theory Reasoning
formal verification	SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
formalization	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
G
graph	A logical framework with a graph meta-language
H
hard typing	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Higher-order Pattern Unification	Adelfa: A System for Reasoning about LF Specifications
I
induction	Automating Induction by Reflection
Inductive Reasoning	Adelfa: A System for Reasoning about LF Specifications
inductive type	Countability of Inductive Types Formalized in the Object-Logic Level
Integrity constraints	Towards a Semantic Framework for Policy Exchange in the Internet
Internet routing	Towards a Semantic Framework for Policy Exchange in the Internet
L
lambda-calculus	Interacting safely with an unsafe environment
Logic	Automating Induction by Reflection
logical framework	A logical framework with a graph meta-language
Logical Frameworks	Interacting safely with an unsafe environment
logical relation	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
M
Mathematical Induction	Automating Induction by Reflection
Meta Level Reasoning	Automating Induction by Reflection
meta logic	Countability of Inductive Types Formalized in the Object-Logic Level
meta-logic	Foundations of the Squirrel meta-logic for reasoning over security protocols
Meta-Theory	Facilitating Meta-Theory Reasoning
MetaCoq	The MetaCoq Project
modularity	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
O
object logic	Countability of Inductive Types Formalized in the Object-Logic Level
P
Policy based routing	Towards a Semantic Framework for Policy Exchange in the Internet
Project	The MetaCoq Project
proof assistant	A logical framework with a graph meta-language Adelfa: A System for Reasoning about LF Specifications
proof strategy	A logical framework with a graph meta-language
proof tactic	A logical framework with a graph meta-language
R
Reasoning	Facilitating Meta-Theory Reasoning
Reflection	Automating Induction by Reflection
S
security protocols	Foundations of the Squirrel meta-logic for reasoning over security protocols
SML	SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
soft typing	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Structural Induction	Automating Induction by Reflection
T
theorem prover	A logical framework with a graph meta-language
translation	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Truth Predicate	Automating Induction by Reflection
type theory	Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
U
user interface	A logical framework with a graph meta-language

Disclaimer | Powered by EasyChair Smart Program