Balat, Vincent; Di Cosmo, Roberto; Fiore, Marcelo Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. (English) Zbl 1325.68045 Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’04, Venice, Italy, January 14–16, 2004. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-729-X). 64-76 (2004). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{V. Balat} et al., in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '04, Venice, Italy, January 14--16, 2004. New York, NY: Association for Computing Machinery (ACM). 64--76 (2004; Zbl 1325.68045) Full Text: DOI
Laurent, Olivier; Tortora de Falco, Lorenzo Slicing polarized additive normalization. (English) Zbl 1069.03056 Ehrhard, Thomas (ed.) et al., Linear logic in computer science. Based on the Azores summer school on linear logic and computer science, St. Miguel, Azores, Portugal, August 30–September 7, 2000. Cambridge: Cambridge University Press (ISBN 0-521-60857-0/pbk). London Mathematical Society Lecture Note Series 316, 247-282 (2004). MSC: 03F52 03B40 68N18 PDFBibTeX XMLCite \textit{O. Laurent} and \textit{L. Tortora de Falco}, Lond. Math. Soc. Lect. Note Ser. 316, 247--282 (2004; Zbl 1069.03056)
Simpson, Alex Computational adequacy for recursive types in models of intuitionistic set theory. (English) Zbl 1056.03015 Ann. Pure Appl. Logic 130, No. 1-3, 207-275 (2004). MSC: 03B70 03B40 03E70 03G30 68Q55 18B25 PDFBibTeX XMLCite \textit{A. Simpson}, Ann. Pure Appl. Logic 130, No. 1--3, 207--275 (2004; Zbl 1056.03015) Full Text: DOI Link
Bunder, M. W.; Seldin, Jonathan P. Variants of the basic calculus of constructions. (English) Zbl 1068.03012 J. Appl. Log. 2, No. 2, 191-217 (2004). Reviewer: Vladimir Komendantsky (Cork) MSC: 03B40 03B70 PDFBibTeX XMLCite \textit{M. W. Bunder} and \textit{J. P. Seldin}, J. Appl. Log. 2, No. 2, 191--217 (2004; Zbl 1068.03012) Full Text: DOI
Pym, David J.; Ritter, Eike Reductive logic and proof-search. Proof theory, semantics, and control. (English) Zbl 1062.03003 Oxford Logic Guides 45; Oxford Science Publications. Oxford: Clarendon Press (ISBN 0-19-852633-4/hbk). xv, 208 p. (2004). Reviewer: G. E. Mints (München) MSC: 03-02 03B20 03F03 03B40 03B70 03F05 03G30 PDFBibTeX XMLCite \textit{D. J. Pym} and \textit{E. Ritter}, Reductive logic and proof-search. Proof theory, semantics, and control. Oxford: Clarendon Press (2004; Zbl 1062.03003)
Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T. Type-based termination of recursive definitions. (English) Zbl 1054.68027 Math. Struct. Comput. Sci. 14, No. 1, 97-141 (2004). Reviewer: Neculai Curteanu (Iaşi) MSC: 68N18 03B40 03B70 68Q65 68Q60 68Q55 68T15 PDFBibTeX XMLCite \textit{G. Barthe} et al., Math. Struct. Comput. Sci. 14, No. 1, 97--141 (2004; Zbl 1054.68027) Full Text: DOI