FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Achermann, Reto	Physical Addressing on Real Hardware in Isabelle/HOL
Anand, Abhishek	Towards Certified Meta-Programming with Typed Template-Coq
Avelar, Andréia B.	Formalizing Ring Theory in PVS (Short Paper)
B
Balco, Samuel	Software Tool Support for Modular Reasoning in Modal Logics of Actions
Bannister, Callum	Backwards and Forwards with Separation Logic
Baston, Colm	The Coinductive Formulation of Common Knowledge
Benzaken, Véronique	A Coq Formalisation of SQL’S Execution Engines
Blair, Richard	Efficient Mendler-Style Lambda-Encodings in Cedille
Boulier, Simon	Towards Certified Meta-Programming with Typed Template-Coq
Boulmé, Sylvain	A Coq Tactic for Equality Learning in Linear Arithmetic
C
C. D. S. Oliveira, Bruno	Formalization of a Polymorphic Subtyping Algorithm
Capretta, Venanzio	The Coinductive Formulation of Common Knowledge
Carette, Jacques	HOL Light QE
Cauderlier, Raphaël	Tactics and Certificates in Meta Dedukti
Chlipala, Adam	Reification by Parametricity
Cock, David	Physical Addressing on Real Hardware in Isabelle/HOL
Cohen, Cyril	Towards Certified Meta-Programming with Typed Template-Coq
Combette, Guillaume	A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
Contejean, Evelyne	A Coq Formalisation of SQL’S Execution Engines
D
Daggitt, Matthew L.	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
de Lima, Thaynara A.	Formalizing Ring Theory in PVS (Short Paper)
Divasón, Jose	A Formalization of the LLL Basis Reduction Algorithm
Doczkal, Christian	A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
E
Eberl, Manuel	Verified Analysis of Random Binary Tree Structures
Erbsen, Andres	Reification by Parametricity
F
Farmer, William	HOL Light QE
Feliu Gabaldon, Marco Antonio	Boosting the Reuse of Formal Specifications
Ferreira, Joao F.	Towards Verified Handwritten Calculational Proofs (Short Paper)
Filliâtre, Jean-Christophe	Deductive Program Verification
Firsov, Denis	Efficient Mendler-Style Lambda-Encodings in Cedille
Forster, Yannick	Verification of PCP-Related Computational Reductions in Coq
Frittella, Sabine	Software Tool Support for Modular Reasoning in Modal Logics of Actions
G
Galdino, André Luiz	Formalizing Ring Theory in PVS (Short Paper)
Garbuzov, Dmitri	A Formal Equational Theory for Call-by-Push-Value
Goertzel, Zarathustra	ProofWatch: Watchlist Guidance for Large Theories in E
Grayson, Daniel R.	Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics
Greco, Giuseppe	Software Tool Support for Modular Reasoning in Modal Logics of Actions
Griffin, Timothy G.	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Gross, Jason	Reification by Parametricity
H
Harper, Robert	Verified Tail Bounds for Randomized Programs
Harrison, John	Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification
Haslbeck, Max W.	Verified Analysis of Random Binary Tree Structures
Heiter, Edith	Verification of PCP-Related Computational Reductions in Coq
Hu, Shuwei	Verified Memoization and Dynamic Programming
Humbel, Lukas	Physical Addressing on Real Hardware in Isabelle/HOL
Höfner, Peter	Backwards and Forwards with Separation Logic
Hölzl, Johannes	MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
J
Jakubuv, Jan	ProofWatch: Watchlist Guidance for Large Theories in E
Jantsch, Simon	Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
Joosten, Sebastiaan	A Formalization of the LLL Basis Reduction Algorithm
K
Kahl, Wolfram	CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
Kaliszyk, Cezary	Towards Formal Foundations for Game Theory (Short Paper)
Keller, Chantal	A Coq Formalisation of SQL’S Execution Engines
Klein, Gerwin	Program Verification in the Presence of Cached Address Translation Backwards and Forwards with Separation Logic
Knüppel, Alexander	Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Kumar, Ramana	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Kurz, Alexander	Software Tool Support for Modular Reasoning in Modal Logics of Actions
L
Larchey-Wendling, Dominique	Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
Laskowski, Patrick	HOL Light QE
Lochbihler, Andreas	Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes Fast Machine Words in Isabelle/HOL
Lopez Pombo, Carlos	Boosting the Reuse of Formal Specifications
M
Martins, Eunice	A Coq Formalisation of SQL’S Execution Engines
Maréchal, Alexandre	A Coq Tactic for Equality Learning in Linear Arithmetic
Mendes, Alexandra	Towards Verified Handwritten Calculational Proofs (Short Paper)
Meßner, Florian	A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Miquey, Étienne	Formalizing Implicative Algebras in Coq
Moscato, Mariano	Boosting the Reuse of Formal Specifications
Mullen, Eric	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Munoz, Cesar	Boosting the Reuse of Formal Specifications
Myreen, Magnus O.	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
N
Nipkow, Tobias	Verified Memoization and Dynamic Programming Verified Analysis of Random Binary Tree Structures
Norrish, Michael	Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
P
Palmigiano, Alessandra	Software Tool Support for Modular Reasoning in Modal Logics of Actions
Pardylla, Carsten	Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Parsert, Julian	A Formally Verified Solver for Homogeneous Linear Diophantine Equations Towards Formal Foundations for Game Theory (Short Paper)
Pizani Flor, João Paulo	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
Pous, Damien	A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
R
Rizkallah, Christine	A Formal Equational Theory for Call-by-Push-Value
Roscoe, Timothy	Physical Addressing on Real Hardware in Isabelle/HOL
S
Schaefer, Ina	Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Schneider, Joshua	Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
Schrijvers, Tom	Formalization of a Polymorphic Subtyping Algorithm
Schulz, Stephan	ProofWatch: Watchlist Guidance for Large Theories in E
Schöpf, Jonas	A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Smolka, Gert	Verification of PCP-Related Computational Reductions in Coq
Sozeau, Matthieu	Towards Certified Meta-Programming with Typed Template-Coq
Sternagel, Christian	A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Stump, Aaron	Efficient Mendler-Style Lambda-Encodings in Cedille
Swierstra, Wouter	Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
Syeda, Hira	Program Verification in the Presence of Cached Address Translation
T
Tabareau, Nicolas	Towards Certified Meta-Programming with Typed Template-Coq
Tassarotti, Joseph	Verified Tail Bounds for Randomized Programs
Tatlock, Zachary	Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
Thiemann, René	A Formalization of the LLL Basis Reduction Algorithm
Thüm, Thomas	Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
U
Urban, Josef	ProofWatch: Watchlist Guidance for Large Theories in E
W
Wimmer, Simon	Verified Memoization and Dynamic Programming MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
Y
Yamada, Akihisa	A Formalization of the LLL Basis Reduction Algorithm
Z
Zdancewic, Steve	A Formal Equational Theory for Call-by-Push-Value
Zhao, Jinxu	Formalization of a Polymorphic Subtyping Algorithm
Zmigrod, Ran	An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory

Disclaimer | Powered by EasyChair Smart Program