FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Agda	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
Asynchronous	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
automated reasoning	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
B
Bar inductive predicates	Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (PDF, talk)
Basis Reduction	A Formalization of the LLL Basis Reduction Algorithm (PDF, talk)
Biform theories	HOL Light QE (PDF, talk)
binary search tree	Verified Analysis of Random Binary Tree Structures (PDF, talk)
C
Cached Address Translation	Program Verification in the Presence of Cached Address Translation (PDF, talk)
calculational method	Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
Calculational proof	CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” (PDF, talk)
call by push value	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Cedille	Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
certificate checking	Tactics and certificates in Meta Dedukti (PDF, talk)
certified code	A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk)
Certified execution engine	A Coq formalisation of SQL’s execution engines (PDF, talk)
certified software	Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk)
Church's type theory	HOL Light QE (PDF, talk)
classical realizability	Formalizing Implicative Algebras in Coq (PDF, talk)
Clause Learning	A Coq Tactic for Equality Learning in Linear Arithmetic (PDF, talk)
code generation	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk) Fast machine words in Isabelle/HOL (PDF, talk) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk)
coinductive types	The Coinductive Formulation of Common Knowledge (PDF, talk)
common knowledge	The Coinductive Formulation of Common Knowledge (PDF, talk)
complete lattices	Formalizing Implicative Algebras in Coq (PDF, talk)
Computational Reductions	Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
Context-free Grammars	Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
contextual equivalence	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Control parameters	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Coq	Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk) A Coq formalisation of SQL’s execution engines (PDF, talk) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk) Reification by Parametricity (PDF, talk) Formalizing Implicative Algebras in Coq (PDF, talk)
Correctness by extraction	Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (PDF, talk)
Cycle finding	Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (PDF, talk)
D
Databases	A Coq formalisation of SQL’s execution engines (PDF, talk)
datatypes	Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk) Boosting the Reuse of Formal Specifications (PDF, talk)
deductive verification	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Dedukti	Tactics and certificates in Meta Dedukti (PDF, talk)
dependent types	Tactics and certificates in Meta Dedukti (PDF, talk) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
dependently typed programming	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
Design by contract	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
domain specific languages	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
dynamic epistemic logic	Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Dynamic Programming	Verified Memoization and Dynamic Programming (PDF, talk)
E
Economics	Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
epistemic logic	The Coinductive Formulation of Common Knowledge (PDF, talk)
equational theory	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Expected Utility	Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
extraction	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk)
F
Formal Methods	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
formal proofs	Formalizing Ring Theory in PVS (short paper) (PDF, talk) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk)
formal verification	Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (PDF, talk) Verified Tail Bounds for Randomized Programs (PDF, talk)
Formalisation	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
functional programming	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk) Formalization of a Polymorphic Subtyping Algorithm (PDF, talk)
functor	Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk)
G
Game Theory	Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
graph minor theorem	A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk)
graph theory	A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk)
H
hammers	ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
handwriting	Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
handwritten mathematics	Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
Hardware model	Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
hardware verification	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
Higher-Ranked Polymorphism	Formalization of a Polymorphic Subtyping Algorithm (PDF, talk)
HOL	Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (PDF, talk)
HOL Light	HOL Light QE (PDF, talk)
homogeneous linear diophantine equations	A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk)
HW-SW interface	Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
I
IDE	Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
implicative algebras	Formalizing Implicative Algebras in Coq (PDF, talk)
induction principle	Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
inductive datatypes	Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
interactive theorem proving	Software tool support for modular reasoning in modal logics of actions (PDF, talk) Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk) Verified Memoization and Dynamic Programming (PDF, talk)
Isabelle	Software tool support for modular reasoning in modal logics of actions (PDF, talk) Verified Analysis of Random Binary Tree Structures (PDF, talk) Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
Isabelle/HOL	Physical addressing on real hardware in Isabelle/HOL (PDF, talk) A Formalization of the LLL Basis Reduction Algorithm (PDF, talk) Fast machine words in Isabelle/HOL (PDF, talk) Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk) Verified Memoization and Dynamic Programming (PDF, talk) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (PDF, talk)
Isabelle/HOL Theorem Proving	Program Verification in the Presence of Cached Address Translation (PDF, talk)
K
KeY	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
L
lambda-encodings	Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
large libraries	ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
Linear Programming	A Coq Tactic for Equality Learning in Linear Arithmetic (PDF, talk)
loop unrolling	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
M
machine words	Fast machine words in Isabelle/HOL (PDF, talk)
Markov decision processes	MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (PDF, talk)
Master Theorem	Verified Tail Bounds for Randomized Programs (PDF, talk)
mathematical proof	Towards Verified Handwritten Calculational Proofs (short paper) (PDF, talk)
Mathematics	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
mechanized mathematics	A Formally Verified Solver for Homogeneous Linear Diophantine Equations (PDF, talk)
Memoization	Verified Memoization and Dynamic Programming (PDF, talk)
Memory	Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
meta programming	Tactics and certificates in Meta Dedukti (PDF, talk)
meta-programming	Towards Certified Meta-Programming with Typed Template-Coq (PDF, talk)
Metareasoning	HOL Light QE (PDF, talk)
MIPS TLB	Physical addressing on real hardware in Isabelle/HOL (PDF, talk)
model checking	Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (PDF, talk)
model-based testing	Fast machine words in Isabelle/HOL (PDF, talk)
N
normal form bisimulation	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
O
observational equivalence	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Operating System Verification	Program Verification in the Presence of Cached Address Translation (PDF, talk)
optimizations	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
P
Parametricity	Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk)
Partial algorithms in Coq	Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (PDF, talk)
Polynomial Factorization	A Formalization of the LLL Basis Reduction Algorithm (PDF, talk)
polytyptic programming	Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk)
Post Correspondence Problem	Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
predecessor function	Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
probabilistic	Verified Analysis of Random Binary Tree Structures (PDF, talk)
Probabilistic Timed Automata	MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (PDF, talk)
probability	Verified Tail Bounds for Randomized Programs (PDF, talk)
Program Verification	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk) Program Verification in the Presence of Cached Address Translation (PDF, talk)
proof assistants	The Coinductive Formulation of Common Knowledge (PDF, talk) HOL Light QE (PDF, talk) Reification by Parametricity (PDF, talk)
proof automation	ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
proof by reflection	Reification by Parametricity (PDF, talk)
proof engineering	Reification by Parametricity (PDF, talk)
proof guidance	ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
proof theory of modal logic	Software tool support for modular reasoning in modal logics of actions (PDF, talk)
Proof-checker	CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” (PDF, talk)
PVS	Formalizing Ring Theory in PVS (short paper) (PDF, talk) Boosting the Reuse of Formal Specifications (PDF, talk)
Q
Quicksort	Verified Analysis of Random Binary Tree Structures (PDF, talk)
Quotation and evaluation	HOL Light QE (PDF, talk)
quotients	Relational parametricity and quotient preservation for modular (co)datatypes (PDF, talk) Boosting the Reuse of Formal Specifications (PDF, talk)
R
randomised	Verified Analysis of Random Binary Tree Structures (PDF, talk)
randomized algorithm	Verified Tail Bounds for Randomized Programs (PDF, talk)
Reasoning about syntax	HOL Light QE (PDF, talk)
refinement	Boosting the Reuse of Formal Specifications (PDF, talk)
Reflection	HOL Light QE (PDF, talk)
reification	Reification by Parametricity (PDF, talk)
rewriting	Tactics and certificates in Meta Dedukti (PDF, talk)
Ring Theory	Formalizing Ring Theory in PVS (short paper) (PDF, talk)
S
Security	Program Verification in the Presence of Cached Address Translation (PDF, talk)
separation logic	Backwards and Forwards with Separation Logic (PDF, talk)
Skeptical Approach	A Coq Tactic for Equality Learning in Linear Arithmetic (PDF, talk)
software verification	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk)
SQL	A Coq formalisation of SQL’s execution engines (PDF, talk)
Ssreflect	A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (PDF, talk)
string rewriting	Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
strongest postcondition	Backwards and Forwards with Separation Logic (PDF, talk)
symbolic computation	HOL Light QE (PDF, talk)
T
tactics	Tactics and certificates in Meta Dedukti (PDF, talk)
tail bound	Verified Tail Bounds for Randomized Programs (PDF, talk)
Teaching computer science with proof assistants	CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” (PDF, talk)
The Coq Proof Assistant	A Coq Tactic for Equality Learning in Linear Arithmetic (PDF, talk)
theorem proving	Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY (PDF, talk)
Timed automata	MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (PDF, talk)
timing transformations	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk)
Translation Lookaside Buffer (TLB)	Program Verification in the Presence of Cached Address Translation (PDF, talk)
treap	Verified Analysis of Random Binary Tree Structures (PDF, talk)
tripos	Formalizing Implicative Algebras in Coq (PDF, talk)
trusted code base	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk)
trusted computing base	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk)
Type Inference	Formalization of a Polymorphic Subtyping Algorithm (PDF, talk)
type theory	The Coinductive Formulation of Common Knowledge (PDF, talk) Efficient Mendler-Style Lambda-Encodings in Cedille (PDF, talk)
U
Ultrametrics	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (PDF, talk)
Undecidability	Verification of PCP-Related Computational Reductions in Coq (PDF, talk)
untyped call by value lambda calculus	A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
Utility Theory	Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
V
validation	Fast machine words in Isabelle/HOL (PDF, talk)
Verification	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (PDF, talk) A Formal Equational Theory for Call-By-Push-Value (PDF, talk)
verified compiler	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) (PDF, talk)
Von Neumann-Morgenstern Utility Theorem	Towards Formal Foundations for Game Theory (short paper) (PDF, talk)
W
watchlist guidance	ProofWatch: Watchlist Guidance for Large Theories in E (PDF, talk)
weakest precondition	Backwards and Forwards with Separation Logic (PDF, talk)

Disclaimer | Powered by EasyChair Smart Program