۱ مطلب با این برچسب
این مقاله به بررسی و فرمالیزه‌کردن قضیه بازگشتی دوم کلینی در حساب لامبدای بی‌نوع می‌پردازد. نویسنده با پیاده‌سازی این مفهوم در اثبات‌گر Rocq، نشان می‌دهد چگونه می‌توان برنامه‌ای ساخت که سورس‌کد خودش را تولید کند (Quine) و ارتباط عمیق آن را با منطق و تئوری اثبات آشکار می‌کند.