VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
ACL2	Development of a Translator from LLVM to ACL2 Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 Modeling Algorithms in SystemC and ACL2 Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems Industrial-Strength Documentation for ACL2
ACL2(r)	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
arctangent	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
auction strategy	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
automated reasoning	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
automated theorem proving	Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
automation	Data Definitions in ACL2 Sedan
C
Clustering	ACL2(ml): Machine-Learning for ACL2
concurrency	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
D
documentation	Industrial-Strength Documentation for ACL2
E
enumerators	Data Definitions in ACL2 Sedan
Executable Formal Models	Development of a Translator from LLVM to ACL2
execution	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
F
Formal verification	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis Industrial-Strength Documentation for ACL2
ForMaRE	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
Functional instantiation	Polymorphic Types In ACL2
G
Guards	ACL2(ml): Machine-Learning for ACL2
H
hardware verification	Modeling Algorithms in SystemC and ACL2
High Level Synthesis	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
L
LLVM	Development of a Translator from LLVM to ACL2
Loop Pipelining Transformation	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
M
Machine-Learning	ACL2(ml): Machine-Learning for ACL2
mechanized proof	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
multiprocessor	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
N
new features	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
non-standard analysis	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
P
pedagogy	Data Definitions in ACL2 Sedan
polymorphism	Data Definitions in ACL2 Sedan Polymorphic Types In ACL2
polynomial approximations	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
R
real analysis	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
S
SSA Form	Development of a Translator from LLVM to ACL2
SystemC	Modeling Algorithms in SystemC and ACL2
T
taylor series	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
test data generation	Data Definitions in ACL2 Sedan
theorem proving	Development of a Translator from LLVM to ACL2 Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
TPTP	Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
type framework	Data Definitions in ACL2 Sedan
type system	Polymorphic Types In ACL2
V
Vickrey's theorem	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
W
weak memory	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
X
XML	Industrial-Strength Documentation for ACL2

Disclaimer | Powered by EasyChair Smart Program