2024/05/07

Newest at the top

2024-05-07 19:25:44 +0200danza(~francesco@151.47.243.64)
2024-05-07 19:25:20 +0200danza(~francesco@151.47.243.64) (Remote host closed the connection)
2024-05-07 19:24:32 +0200justsomeguy(~justsomeg@user/justsomeguy) (Ping timeout: 268 seconds)
2024-05-07 19:23:33 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds)
2024-05-07 19:23:24 +0200madariaga(~madariaga@user/madariaga)
2024-05-07 19:22:30 +0200danza(~francesco@151.47.243.64)
2024-05-07 19:22:15 +0200AlexZenon(~alzenon@178.34.162.125)
2024-05-07 19:22:01 +0200danza(~francesco@151.47.243.64) (Remote host closed the connection)
2024-05-07 19:21:59 +0200Rodney_(~Rodney@176.254.244.83) (Ping timeout: 252 seconds)
2024-05-07 19:21:57 +0200xal(~xal@mx1.xal.systems)
2024-05-07 19:20:49 +0200xal(~xal@mx1.xal.systems) (Client Quit)
2024-05-07 19:20:44 +0200xal(~xal@mx1.xal.systems)
2024-05-07 19:19:57 +0200Mach(~Mach@86.127.202.233) (Ping timeout: 255 seconds)
2024-05-07 19:19:14 +0200danza(~francesco@151.47.243.64)
2024-05-07 19:18:49 +0200euphores(~SASL_euph@user/euphores)
2024-05-07 19:17:59 +0200AlexZenon(~alzenon@178.34.162.125) (Ping timeout: 264 seconds)
2024-05-07 19:16:28 +0200paddymahoney(~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com)
2024-05-07 19:16:14 +0200Square(~Square@user/square)
2024-05-07 19:15:27 +0200xal(~xal@mx1.xal.systems) ()
2024-05-07 19:15:20 +0200paddymahoney(~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 260 seconds)
2024-05-07 19:05:32 +0200madariaga(~madariaga@user/madariaga) (Ping timeout: 260 seconds)
2024-05-07 19:04:23 +0200Square3(~Square4@user/square) (Ping timeout: 252 seconds)
2024-05-07 19:01:42 +0200chexum(~quassel@gateway/tor-sasl/chexum)
2024-05-07 19:01:14 +0200chexum(~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds)
2024-05-07 19:01:06 +0200madariaga(~madariaga@user/madariaga)
2024-05-07 18:57:09 +0200dostoyevsky2(~sck@user/dostoyevsky2)
2024-05-07 18:53:18 +0200rosco(~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal)
2024-05-07 18:52:53 +0200dostoyevsky2(~sck@user/dostoyevsky2) (Ping timeout: 240 seconds)
2024-05-07 18:49:29 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-05-07 18:44:29 +0200tri(~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 240 seconds)
2024-05-07 18:42:11 +0200philopsos(~caecilius@user/philopsos)
2024-05-07 18:40:07 +0200tri(~tri@ool-18bbef1a.static.optonline.net)
2024-05-07 18:39:07 +0200tzh(~tzh@c-73-164-206-160.hsd1.or.comcast.net)
2024-05-07 18:31:49 +0200 <ski> Twelf <https://twelf.org/>
2024-05-07 18:31:25 +0200 <ski> lambdaProlog <https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/>,Lolli <https://www.lix.polytechnique.fr/Labo/Dale.Miller/lolli/>
2024-05-07 18:31:17 +0200demon-cat(~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net)
2024-05-07 18:30:55 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-05-07 18:30:03 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-05-07 18:29:54 +0200 <ski> (Lolli is a version of lambdaProlog using linear logic. it is dynamically typed)
2024-05-07 18:29:37 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-05-07 18:29:35 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1))
2024-05-07 18:29:18 +0200euleritian(~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer)
2024-05-07 18:28:47 +0200 <ski> however, iirc, there's an implementation of (a restriction of) Lolli (called LolliMon, iirc), which uses a more Prolog-like syntax (uncurried rather than curried predicates), which doesn't have lambda-terms, but does have implication and universal quantification goals, so evidently people considered the latter two useful even without the former
2024-05-07 18:28:42 +0200ubert(~Thunderbi@2a02:8109:ab8a:5a00:f7fe:a5d:216b:79ee) (Remote host closed the connection)
2024-05-07 18:28:41 +0200euleritian(~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de)
2024-05-07 18:28:27 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
2024-05-07 18:28:19 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
2024-05-07 18:28:17 +0200philopsos(~caecilius@user/philopsos) (Quit: Lost terminal)
2024-05-07 18:26:47 +0200 <ski> if one consider the HOAS representation (including some kind of unification of lambda terms, up to alpha, beta, and eta conversion) a killer feature of lambdaProlog (and Twelf), then that's the reason it also has implicational goals, and universal quantification goals, because without the latter two, the first one is not as useful
2024-05-07 18:24:35 +0200 <ski> it also has parametric polymorphism, but no dependent types