TTT 2017 Contributors -

Wed 18 - Fri 20 January 2017

co-located with POPL 2017

Filter

Role Type

Contributing to

Number of Roles

Country

Results (23)

A Andreas AbelAbel, Andreas Gothenburg University Committee Member in Program Committee within the TTT-track
Guillaume AllaisAllais, Guillaume Radboud University NijmegenFrance agdARGS - Declarative Hierarchical Command Line Interfaces
B Andrej BauerBauer, Andrej University of LjubljanaSlovenia Committee Member in Program Committee within the TTT-track
H Hugo HerbelinHerbelin, Hugo Session Chair of Second Afternoon Session (part of TTT) Coq's Prolog and application to defining semi-automatic tactics
K Jonas KaiserKaiser, Jonas Equivalence of System F and λ2 in Abella
Steven KeuchelKeuchel, Steven Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding
Robbert KrebbersKrebbers, Robbert Delft University of Technology, NetherlandsNetherlands Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq
M Assia MahboubiMahboubi, Assia INRIAFrance Session Chair of First Morning Session (part of TTT) Committee Member in Program Committee within the TTT-track
Cyprien ManginMangin, Cyprien Equations: a tool for dependent pattern-matching
Koar MarntirosianMarntirosian, Koar Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding
Alberto MomiglianoMomigliano, Alberto A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method
Anders MörtbergMörtberg, Anders Inria Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom
N Keiko NakataNakata, Keiko Germany Session Chair of Second Morning Session (part of TTT) Committee Member in Program Committee within the TTT-track
P Brigitte PientkaPientka, Brigitte McGill University A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method
S Tom SchrijversSchrijvers, Tom KU Leuven Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding
Gert SmolkaSmolka, Gert Saarland University Equivalence of System F and λ2 in Abella
Matthieu SozeauSozeau, Matthieu InriaFrance Equations: a tool for dependent pattern-matching
Bas SpittersSpitters, Bas Session Chair of First Afternoon Session (part of TTT)
T David ThibodeauThibodeau, David McGill University, Canada A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method
Aaron TombTomb, Aaron Galois, Inc.United States Invited Talk -- Type Theory in the Software Analysis Workbench
V Milena Vujosevic JanicicVujosevic Janicic, Milena Modelling Program Behaviour within Software Verification Tool LAV
Z Beta ZilianiZiliani, Beta FAMAF, UNC (Argentina) / CONICET (Argentina)Argentina Introducing MetaCoq: A Safe Tactic Language for Coq
Théo ZimmermannZimmermann, Théo IRIF, Université Paris DiderotFrance Coq's Prolog and application to defining semi-automatic tactics