Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's \lambda\_mu\_{\~mu}-calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed lambda-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiri...
Kaydedildi:
| Asıl Yazarlar: | , , |
|---|---|
| Materyal Türü: | Artigo |
| Dil: | Inglês |
| Baskı/Yayın Bilgisi: |
Logical Methods in Computer Science e.V.
2009-05-01
|
| Seri Bilgileri: | Logical Methods in Computer Science |
| Konular: | |
| Online Erişim: | https://lmcs.episciences.org/1149/pdf |
| Etiketler: |
Etiket eklenmemiş, İlk siz ekleyin!
|