Yes. Among the most recent attempts is Homotopy Type Theory and the "Univalent Foundations" program (check out The HoTT Book). It's based on Martin Löf's version of type theory (here's a nice nLab article on it: Martin-Löf dependent type theory).