FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

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

Disclaimer | Powered by EasyChair Smart Program