!LADvlewaWOnmvMkjxE:matrix.org

Applied Category Theory

285 Members
19 Servers

Load older messages

Timestamp Message
21 Jan 2020
03:41:51@telegram_897557541:t2bot.ioPhilip Zuckerah.
03:41:55@telegram_897557541:t2bot.ioPhilip ZuckerI just happened to see this
03:41:56@telegram_897557541:t2bot.ioPhilip Zucker https://hackage.haskell.org/package/z3
03:42:03@telegram_897557541:t2bot.ioPhilip ZuckerBy snooping what conal elliott was up to on github
03:42:13@telegram_687038879:t2bot.iotopos https://hackage.haskell.org/package/sbv
03:42:18@telegram_687038879:t2bot.iotoposthis is the big boi lib
03:42:33@telegram_687038879:t2bot.iotoposlevent erkok's fine work
03:42:37@telegram_897557541:t2bot.ioPhilip Zuckersbv seems phenomenol
03:43:24@telegram_897557541:t2bot.ioPhilip ZuckerI was fiddling with it as a backend for a relation algebra thingo, but I think it doesn't support the full set of quantifiers the way the real z3 bindings do
03:43:58@telegram_897557541:t2bot.ioPhilip ZuckerBut I am seriously impressed by how thoughtfully its been made
03:44:10@telegram_897557541:t2bot.ioPhilip ZuckerI guess it took a long time
03:44:23@telegram_687038879:t2bot.iotoposyeah, many many versions 🙂
03:44:34@telegram_687038879:t2bot.iotoposthe haskell interface is 10/10
03:44:37@telegram_687038879:t2bot.iotopos* the haskell interface is 10/10
03:47:27@telegram_687038879:t2bot.iotoposanyway, my application is in. Hopefully that gets through the relevant filters
03:49:25@telegram_277202990:t2bot.ioRashad Gover joined the room.
03:49:58@telegram_897557541:t2bot.ioPhilip Zuckerthere is no butting happening. 😁
03:50:09@telegram_897557541:t2bot.ioPhilip ZuckerWell that tutorial I posted is shaping up
03:50:23@telegram_277202990:t2bot.ioRashad Gover @topos Hope you get the job btw!!
03:50:31@telegram_897557541:t2bot.ioPhilip Zuckerbut even if it isn't the links at the end are the best stuff I know of
03:51:19@telegram_897557541:t2bot.ioPhilip Zucker rise4fun https://rise4fun.com/z3/tutorialcontent/guide
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
Programming Z3 - https://theory.stanford.edu/~nikolaj/programmingz3.html
Hakank's examples http://www.hakank.org/z3/
Yurichev's book "SMT by Example" https://yurichev.com/writings/SAT_SMT_by_example.pdf

http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/
http://hackage.haskell.org/package/sbv
https://www.youtube.com/watch?v=ruNFcH-KibY Tikhon Jelvis - Analyzing Programs with Z3
03:51:26@telegram_897557541:t2bot.ioPhilip Zuckerquite a load
03:51:46@telegram_277202990:t2bot.ioRashad Gover Philip Haha😁 good. Thank you so much! I’m trying be like you all.
03:52:10@telegram_503372818:t2bot.ioGNU/Brett G. https://t.me/joinchat/HgDcEk6Z5tRiYvrm3dL23Q
03:52:30@telegram_277202990:t2bot.ioRashad Gover @brettmg thank you!
03:55:05@telegram_503372818:t2bot.ioGNU/Brett G.
In reply to Rashad Gover
@brettmg thank you!
:)
03:56:35@telegram_897557541:t2bot.ioPhilip ZuckerI am filled with warm fuzzies 😊
07:44:14@telegram_201226859:t2bot.ioFo Uche
In reply to topos
@brettmg I'm a professional haskeller by trade, and I do a fair bit of mathematics, and I'm looking to enter into more of a research capacity to make sure I can focus on it. In fact, I'm just about to publish with a few people from the ACT group including @Fo_uche! I've been working with haskell and coq and a few other theorem provers now for years. My current employer has me maintaining a language which interfaces with Z3 as a feature (think types and verification a la curry)
Hi! 🐼
07:56:25@telegram_812273871:t2bot.iokl mw
In reply to GNU/Brett G.
Cus my place might be hiring soon graduate students, and post-docs in computer science or mathematics who have good experience with OCaml, Scheme, or Haskell.
What is your place?
08:22:28@telegram_220382467:t2bot.ioIla changed their display name from Sensei to Ila.

There are no newer messages yet.

Back to Room List