Janus Troelsen
#neuhier I previously lived in Darmstadt, but now I live in Mexico. I participate in a Discord-based reading group for the Types and Programming Languages book, we just finished covering Simply Typed Lambda Calculus. If interesting, please let me know and I can help get you up to speed and you can join us.
Mar 17 at 10:14pmWeb
Show threadBoyd Stephen Smith Jr.Mar 17

@janus I've been though most of TAPL independently. If you want to play around with an (untyped) lambda calculus evaluator, I have one on my website: https://www.iguanasuicide.net/

With sources available: https://gitlab.com/bss03/halogen-lambda

I might tear it down soon to replace it with a CEK machine instead of evaluation-by-substitution, but I still want to have it as a interactive LC toy as I try to write my own GRTT implementation.

Development

Show threadcrossgolf_rebel - kostenlose KwalitätspostsMar 18
@janus Hello and welcome to the #Fediverse ​​

The network where so much more is possible than many people even realise
https://fediversum.info/
Willkommen im Fediverse!

Informationen zum dezentralen Netzwerk Fediverse. Entdecke ein Netzwerk aus Millionen von Menschen, behalte die volle Kontrolle über deine Daten, ohne Tracking!

fediversum.info
Show threadHoldMyTypeMar 18
@janus how about stratified lambda calculus - axiom of restricted comprehension?
Show threadHoldMyTypeMar 18
System F stratification — polymorphic λ-calculus where types and terms live at different levels
Predicative stratification — Coq/Agda style universes (Type₀ : Type₁ : Type₂ ...) to avoid Girard's paradox
Elementary Affine Logic / Bounded Linear Logic — stratification to control complexity (terms reduce in bounded time
/Quasi related /not vetted
https://mathstodon.xyz/@xameer/116249300428180520
HoldMyType (@[email protected])

@[email protected] how about stratified lambda calculus - axiom of restricted comprehension?

Mathstodon
Show threadJanus TroelsenMar 18
@xameer sounds interesting. I don't think Pierce covers it, but do you know of a textbook that does?
Show threadHoldMyTypeMar 18
@janus
I only read some paper when I used twitter and was reading on quine's new foundation on math
in context of how different set theories related lambda calculus and then type theory, too many functional pearls texts ( not books)
https://randall-holmes.github.io/
Yes this was the guy , very cool cool texts what's the URL to discord thing?
I ll join it after the job hunt
Edited
Show threadnebunez Mar 18
@janus Hey, this seems interesting to me!