Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Quantum Computations and HoTT
@ 2018-12-14  4:06 José Manuel Rodriguez Caballero
       [not found] ` <20181214071146.GA19128@pachax.iitpkd.ac.in>
                   ` (2 more replies)
  0 siblings, 3 replies; 4+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-12-14  4:06 UTC (permalink / raw)
  To: HomotopyTypeTheory

[-- Attachment #1: Type: text/plain, Size: 666 bytes --]

Hello,
  I am interested in the formal verification of theorems related to Quantum
Computations. I have two possibilities in order to do my formalizations:
either I can use simple type theory (Isabelle/HOL) or I can use UniMath
(Coq). Does the homotopy type theory has some advantage over the simple
type theory in this field?

Kind Regards,
José M.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 944 bytes --]

^ permalink raw reply	[flat|nested] 4+ messages in thread

end of thread, other threads:[~2018-12-21  4:10 UTC | newest]

Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-12-14  4:06 [HoTT] Quantum Computations and HoTT José Manuel Rodriguez Caballero
     [not found] ` <20181214071146.GA19128@pachax.iitpkd.ac.in>
2018-12-17  3:06   ` José Manuel Rodriguez Caballero
2018-12-21  4:09 ` David Roberts
     [not found] ` <CAFL+ZM9aN8ZuPb8TAXjqR1CJ5t2euwaFGBksu=B9FcUc_x1ghg@mail.gmail.com>
2018-12-21  4:10   ` José Manuel Rodriguez Caballero

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).