Powered by
2017 European Joint Conferences on Theory and Practice of Software (ETAPS),
April 22–29, 2017,
Uppsala, Sweden
ESOP
Probabilistic Programming
Tue, Apr 25, 14:00 - 16:00, Sal B
Graph Rewriting
Wed, Apr 26, 09:00 - 10:00, Sal B
Confluence of Graph Rewriting with Interfaces
Filippo Bonchi,
Fabio Gadducci ,
Aleks Kissinger, Pawel Sobocinski, and
Fabio Zanasi
(ENS Lyon, France; University of Pisa, Italy; Radboud University Nijmegen, Netherlands; University of Southampton, UK; University College London, UK)
@InProceedings{ETAPS17p397,
author = {Filippo Bonchi and Fabio Gadducci and Aleks Kissinger and Pawel Sobocinski and Fabio Zanasi},
title = {Confluence of Graph Rewriting with Interfaces},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Incremental Update for Graph Rewriting
Pierre Boutillier, Thomas Ehrhard, and
Jean Krivine
(Harvard Medical School, USA; University of Paris Diderot, France; CNRS, France; amp, France)
@InProceedings{ETAPS17p496,
author = {Pierre Boutillier and Thomas Ehrhard and Jean Krivine},
title = {Incremental Update for Graph Rewriting},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Concurrency
Wed, Apr 26, 10:30 - 12:30, Sal B
Abstract Specifications for Concurrent Maps
Shale Xiong,
Pedro da Rocha Pinto, Gian Ntzik, and
Philippa Gardner
(Imperial College London, UK)
@InProceedings{ETAPS17p595,
author = {Shale Xiong and Pedro da Rocha Pinto and Gian Ntzik and Philippa Gardner},
title = {Abstract Specifications for Concurrent Maps},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Info
Caper - Automatic Verification for Fine-Grained Concurrency
Thomas Dinsdale-Young,
Pedro da Rocha Pinto,
Kristoffer Just Andersen, and
Lars Birkedal
(Aarhus University, Denmark; Imperial College London, UK)
@InProceedings{ETAPS17p694,
author = {Thomas Dinsdale-Young and Pedro da Rocha Pinto and Kristoffer Just Andersen and Lars Birkedal},
title = {Caper - Automatic Verification for Fine-Grained Concurrency},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Video
Info
Language Design
Wed, Apr 26, 14:00 - 16:00, Sal B
Disjoint Polymorphism
João Alpuim,
Bruno C. d. S. Oliveira , and Zhiyuan Shi
(University of Hong Kong, China)
@InProceedings{ETAPS17p1090,
author = {João Alpuim and Bruno C. d. S. Oliveira and Zhiyuan Shi},
title = {Disjoint Polymorphism},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
The Essence of Functional Programming on Semantic Data
Martin Leinberger,
Ralf Lämmel, and Steffen Staab
(University of Koblenz-Landau, Germany; University of Southampton, UK)
@InProceedings{ETAPS17p1288,
author = {Martin Leinberger and Ralf Lämmel and Steffen Staab},
title = {The Essence of Functional Programming on Semantic Data},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Verification
Wed, Apr 26, 16:30 - 18:00, Sal B
Is Your Software on Dope? Formal Analysis of Surreptitiously "enhanced" Programs
Pedro R. D'Argenio, Gilles Barthe,
Sebastian Biewer, Bernd Finkbeiner, and
Holger Hermanns
(Universidad Nacional de Córdoba, Argentina; CONICET, Argentina; Saarland University, Germany; IMDEA Software Institute, Spain)
@InProceedings{ETAPS17p1387,
author = {Pedro R. D'Argenio and Gilles Barthe and Sebastian Biewer and Bernd Finkbeiner and Holger Hermanns},
title = {Is Your Software on Dope? Formal Analysis of Surreptitiously "enhanced" Programs},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Tim Wood, Sophia Drossopolou
,
Shuvendu K. Lahiri , and Susan Eisenbach
(Imperial College London, UK; Microsoft Research, USA)
@InProceedings{ETAPS17p1486,
author = {Tim Wood and Sophia Drossopolou and Shuvendu K. Lahiri and Susan Eisenbach},
title = {Modular Verification of Procedure Equivalence in the Presence of Memory Allocation},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency
Ahmed Bouajjani,
Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, and Serdar Tasiran
(University of Paris Diderot, France; Nokia Bell Labs, USA; Koç University, Turkey)
@InProceedings{ETAPS17p1585,
author = {Ahmed Bouajjani and Michael Emmi and Constantin Enea and Burcu Kulahcioglu Ozkan and Serdar Tasiran},
title = {Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Automated Verification
Thu, Apr 27, 10:30 - 12:30, Sal B
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Hao Tang, Di Wang,
Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, and Lu Zhang
(Peking University, China; University of Texas at Dallas, USA; University of Texas at San Antonio, USA)
@InProceedings{ETAPS17p1684,
author = {Hao Tang and Di Wang and Yingfei Xiong and Lingming Zhang and Xiaoyin Wang and Lu Zhang},
title = {Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Info
Faster Algorithms for Weighted Recursive State Machines
Krishnendu Chatterjee
,
Bernhard Kragl,
Samarth Mishra, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
@InProceedings{ETAPS17p1783,
author = {Krishnendu Chatterjee and Bernhard Kragl and Samarth Mishra and Andreas Pavlogiannis},
title = {Faster Algorithms for Weighted Recursive State Machines},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
ML and Extended Branching VASS
Conrad Cotton-Barratt,
Andrzej S. Murawski, and C.-H. Luke Ong
(University of Oxford, UK; University of Warwick, UK)
@InProceedings{ETAPS17p1882,
author = {Conrad Cotton-Barratt and Andrzej S. Murawski and C.-H. Luke Ong},
title = {ML and Extended Branching VASS},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Theorem Proving
Thu, Apr 27, 14:00 - 16:00, Sal B
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants
Jasmin Christian Blanchette, Aymeric Bouzy,
Andreas Lochbihler,
Andrei Popescu, and
Dmitriy Traytel
(Inria, France; LORIA, France; Max Planck Institute for Informatics, Germany; École Polytechnique, France; ETH Zurich, Switzerland; Middlesex University, UK)
@InProceedings{ETAPS17p2179,
author = {Jasmin Christian Blanchette and Aymeric Bouzy and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel},
title = {Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Info
Verified Characteristic Formulae for CakeML
Armaël Guéneau ,
Magnus O. Myreen , Ramana Kumar, and
Michael Norrish
(ENS Lyon, France; Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia)
@InProceedings{ETAPS17p2377,
author = {Armaël Guéneau and Magnus O. Myreen and Ramana Kumar and Michael Norrish},
title = {Verified Characteristic Formulae for CakeML},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Separation Logic
Fri, Apr 28, 10:30 - 12:30, Sal B
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti,
Ralf Jung , and
Robert Harper
(Carnegie Mellon University, USA; MPI-SWS, Germany)
@InProceedings{ETAPS17p2476,
author = {Joseph Tassarotti and Ralf Jung and Robert Harper},
title = {A Higher-Order Logic for Concurrent Termination-Preserving Refinement},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
The Essence of Higher-Order Concurrent Separation Logic
Robbert Krebbers ,
Ralf Jung ,
Aleš Bizjak, Jacques-Henri Jourdan,
Derek Dreyer , and
Lars Birkedal
(Delft University of Technology, Netherlands; MPI-SWS, Germany; Aarhus University, Denmark)
@InProceedings{ETAPS17p2674,
author = {Robbert Krebbers and Ralf Jung and Aleš Bizjak and Jacques-Henri Jourdan and Derek Dreyer and Lars Birkedal},
title = {The Essence of Higher-Order Concurrent Separation Logic},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan,
Christoph Matheja,
Thomas Noll, and Florian Zuleger
(RWTH Aachen University, Germany; Vienna University of Technology, Austria)
@InProceedings{ETAPS17p2773,
author = {Christina Jansen and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
title = {Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Session Types
Fri, Apr 28, 14:00 - 16:00, Sal B
Linearity, Control Effects, and Behavioural Types
Luis Caires and
Jorge A. Pérez
(Nova University of Lisbon, Portugal; University of Groningen, Netherlands)
@InProceedings{ETAPS17p2971,
author = {Luis Caires and Jorge A. Pérez},
title = {Linearity, Control Effects, and Behavioural Types},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Proving Linearizability Using Partial Orders
Artem Khyzha,
Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson
(IMDEA Software Institute, Spain; University of York, UK; Microsoft Research, UK)
@InProceedings{ETAPS17p3070,
author = {Artem Khyzha and Mike Dodds and Alexey Gotsman and Matthew J. Parkinson},
title = {Proving Linearizability Using Partial Orders},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Type Theory
Fri, Apr 28, 16:30 - 18:00, Sal B
A Classical Sequent Calculus with Dependent Types
Étienne Miquey
(Inria, France; IRIF, France; University of Paris Diderot, France; University of the Republic, Uruguay)
@InProceedings{ETAPS17p3268,
author = {Étienne Miquey},
title = {A Classical Sequent Calculus with Dependent Types},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
Lincx: A Linear Logical Framework with First-Class Contexts
Aina Linn Georges, Agata Murawska, Shawn Otis, and
Brigitte Pientka
(McGill University, Canada; IT University of Copenhagen, Denmark)
@InProceedings{ETAPS17p3367,
author = {Aina Linn Georges and Agata Murawska and Shawn Otis and Brigitte Pientka},
title = {Lincx: A Linear Logical Framework with First-Class Contexts},
booktitle = {Proc.\ ETAPS},
publisher = {Springer},
year = {2017},
}
Publisher's Version
proc time: 6.2