FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program