Travelled to:1 × Croatia
1 × Greece
1 × United Kingdom
2 × Poland
Collaborated with:P.Pédrot P.Melliès M.Sozeau R.Douence A.Hirschowitz T.Hirschowitz G.Jaber C.Tasson Gaëtan Gilbert J.Cockx Simon Boulier Yannick Forster 0002 Théo Winterhalter
Talks about:type (4) coq (4) theori (3) modal (2) substitut (1) hypothesi (1) exponenti (1) homotopi (1) explicit (1) categori (1)
Person: Nicolas Tabareau
DBLP: Tabareau:Nicolas
Contributed to:
2015
2014
2012
20092007
2018
20192020Wrote 9 papers:
- TLCA-2015-HirschowitzHT #type system
- Wild ω-Categories for the Homotopy Hypothesis in Type Theory (AH, TH, NT), pp. 226–240.
- PPDP-2014-DouenceT #imperative #programming
- Lazier Imperative Programming (RD, NT), pp. 7–18.
- LICS-2012-JaberTS #type system
- Extending Type Theory with Forcing (GJ, NT, MS), pp. 395–404.
- ICALP-v2-2009-MelliesTT #exponential #linear #logic
- An Explicit Formula for the Free Exponential Modality of Linear Logic (PAM, NT, CT), pp. 247–260.
- LICS-2007-MelliesT #game studies #semantics
- Resource modalities in game semantics (PAM, NT), pp. 389–398.
- ESOP-2018-PedrotT #type system
- Failure is Not an Option - An Exceptional Type Theory (PMP, NT), pp. 245–271.
- POPL-2019-GilbertCST
- Definitional proof-irrelevance without K (GG, JC, MS, NT), p. 28.
- POPL-2020-PedrotT #how
- The fire triangle: how to mix substitution, dependent elimination, and effects (PMP, NT), p. 28.
- POPL-2020-SozeauBFTW #coq #exclamation #type checking #verification
- Coq Coq correct! verification of type checking and erasure for Coq, in Coq (MS, SB, YF0, NT, TW), p. 28.