coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stefan Ciobaca <stefan.ciobaca AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] algorithm complexity in Coq
- Date: Tue, 19 Mar 2019 15:49:14 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stefan.ciobaca AT gmail.com; spf=Pass smtp.mailfrom=stefan.ciobaca AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f169.google.com
- Ironport-phdr: 9a23:OVXExBVSxfIQn/ejZIZ3LoXVUnPV8LGtZVwlr6E/grcLSJyIuqrYYxGAt8tkgFKBZ4jH8fUM07OQ7/m4HzRZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5uIBmssQndq9QdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAfcdPelGoYnyvV0OpgagCAmtA+Pg0SVHiWPs0qYn1OkhCh3G0xIuH90UtnTYtsn6NKYVUe+u1qbH0S/MYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7LgFWXrIzqJTKV1uIVvmeF8eVgUeOvi3U9pwF3vDev2sEhgZTKiIIN0l3I6zl1zYIvKdC7SEN3e8CoHIVOuy2AKod7Q8cvTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCN4h35VeaRJS50hGtmeL6inhqy/1Wsx+z4W8Wu31ZKqS1FktbItn8TzRDc9s+HSv5l8keg3zaAyRzT5/laLUwokafXMZ0sz74qmpYNr0jPADX6lFj3gaKSbkkk//Kn6+XjYrXovJ+cMIp0hxnlMqQyhMO/D/43Mg4UU2eH+OS806bs8lflT7pQlfA2nazZv4rbJcQfvKK2HwhV0oM75xalEzimyMgYnWUALF9dZB2HiJHpN0jSL/D8EPewmE+hkCxrxvDDJr3uGI/BLnnFkLf7fLZy8VRQyAQpzYMX25UBAbYYZfn3R0XZtdrCDxZ/PRbn7fzgDYBGyo4QUGTHKa6eOqrZuBfc/f4iLeCKIoQUvzz0IPEN6PvnjHt/klgYK/r6laALYWy1S6w1a36SZmDh149YQDU6+zEmRemvs2WsFDtaZnK8RaU5v2hpB4evDIOFTYeo0uXYgHWLW6ZOb2UDMWiiVG/yftzdCfgJYSOWZMRml25cDOXze8oazRir8TTC5f9nI+7ToHNKsJvi0J1s5LSWm0hspHp7CMOS12zLRGZxzDsF
Dear all,
I'm looking for work related to formalized complexity analysis of algorithms in the Word RAM model.
Something along the lines of http://www.eelis.net/research/quicksort/, but where the algorithm is formalized as a Word RAM machine, instead of using a shallow embedding. I would also be interested in other models of computation (e.g., Turing machines), preferably coming with a framework for reasoning in the model.
I would appreciate pointers to any related item.
Best,
Stefan
Stefan
- [Coq-Club] algorithm complexity in Coq, Stefan Ciobaca, 03/19/2019
- Re: [Coq-Club] algorithm complexity in Coq, Bas Spitters, 03/19/2019
Archive powered by MHonArc 2.6.18.