WITS 2022 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (42)

A Guillaume AllaisAllais, Guillaume University of St AndrewsUnited Kingdom Using Dependent Types at Scale: Maintaining the Agda Standard Library
Bernardo AlmeidaAlmeida, Bernardo LASIGE, Faculty of Sciences, University of Lisbon Deciding type equivalence with simple grammars
B Lars BirkedalBirkedal, Lars Aarhus University mitten: A Flexible Multimodal Proof Assistant
William J. BowmanBowman, William J. University of British ColumbiaCanada Committee Member in Program Committee within the WITS-track
C Paulo CanelasCanelas, Paulo LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Jesper CockxCockx, Jesper TU DelftNetherlands Session Chair of Session 1 (part of WITS) Session Chair of Session 2 (part of WITS) Session Chair of Session 4 (part of WITS) Session Chair of Session 5 (part of WITS) Session Chair of Session 3 (part of WITS) Fancy module systems (discussion) Elaborator reflection APIs (discussion) Organizer in Program Committee within the WITS-track
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)
D Matthew L. DaggittDaggitt, Matthew L. Heriot-Watt University Using Dependent Types at Scale: Maintaining the Agda Standard Library
João DavidDavid, João LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Leonardo de Mourade Moura, Leonardo Microsoft Research, n.n. Committee Member in Program Committee within the WITS-track
E Richard A. EisenbergEisenberg, Richard A. TweagFrance Session Chair of Session 1 (part of WITS) Session Chair of Session 2 (part of WITS) Session Chair of Session 4 (part of WITS) Session Chair of Session 5 (part of WITS) Session Chair of Session 3 (part of WITS) Invisible arguments: language design (discussion) Type-aware equational rewriting (discussion) Organizer in Program Committee within the WITS-track
Guilherme EspadaEspada, Guilherme LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
F Alcides FonsecaFonseca, Alcides LASIGE, Faculdade de Ciências da Universidade de LisboaPortugal Understandable and Useful Error Messages for Liquid Types
Yannick ForsterForster, Yannick InriaFrance The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
G Catarina GamboaGamboa, Catarina LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Jad Elkhaleq GhalayiniGhalayini, Jad Elkhaleq University of CambridgeUnited Kingdom Typechecking up to Congruence
Sebastian GrafGraf, Sebastian Karlsruhe Institute of TechnologyGermany Tries that match
Daniel GratzerGratzer, Daniel Aarhus UniversityDenmark mitten: A Flexible Multimodal Proof Assistant
K András KovácsKovács, András Eötvös Loránd University Committee Member in Program Committee within the WITS-track
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom CN: A Refinement Type System for C
L Meven Lennon-BertrandLennon-Bertrand, Meven Inria – LS2N, Université de NantesFrance À bas l’η — Coq’s troublesome η-conversion The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
Yao LiLi, Yao University of PennsylvaniaUnited States The Expression Problem and Theorem Proving (discussion)
M Dhruv MakwanaMakwana, Dhruv University of Cambridge CN: A Refinement Type System for C
Hidehiko MasuharaMasuhara, Hidehiko Tokyo Institute of TechnologyJapan Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)
Kayvan MemarianMemarian, Kayvan University of CambridgeUnited Kingdom CN: A Refinement Type System for C
Andreia MordidoMordido, Andreia Lasige / Faculty of Sciences, Universidade de Lisboa Deciding type equivalence with simple grammars
Reed MullanixMullanix, Reed University of Minnesota Setting the Record Straight with Singletons
P Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus University CN: A Refinement Type System for C
Christopher PultePulte, Christopher University of Cambridge, UK CN: A Refinement Type System for C
Pierre-Marie PédrotPédrot, Pierre-Marie INRIA Committee Member in Program Committee within the WITS-track
R Nick RiouxRioux, Nick University of Pennsylvania The Expression Problem and Theorem Proving (discussion)
S Peter SewellSewell, Peter University of CambridgeUnited Kingdom CN: A Refinement Type System for C
Matthieu SozeauSozeau, Matthieu InriaFrance The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
Philipp StassenStassen, Philipp Aarhus University mitten: A Flexible Multimodal Proof Assistant
Jonathan SterlingSterling, Jonathan Aarhus UniversityDenmark Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
Aaron StumpStump, Aaron The University of Iowa, USAUnited States Committee Member in Program Committee within the WITS-track
T Syouki TsuyamaTsuyama, Syouki Tokyo Institute of Technology Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)
U Sebastian UllrichUllrich, Sebastian Karlsruhe Institute of TechnologyGermany Gotta prove fast: building an ecosystem for effortless native compilation of tactics
V Vasco T. VasconcelosVasconcelos, Vasco T. LASIGE, Faculty of Sciences, University of LisbonPortugal Deciding type equivalence with simple grammars
Niki VazouVazou, Niki IMDEA Software Institute Committee Member in Program Committee within the WITS-track
W Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States The Expression Problem and Theorem Proving (discussion) Benchmarking Binding (discussion)
Z Tesla ZhangZhang, Tesla The Pennsylvania State University Multi case trees: confluence and coverage (discussion) First-class pattern synonyms