Crafa, Silvia; Di Pirro, Matteo; Zucca, Elena Is Solidity solid enough? (English) Zbl 1520.91442 Bracciali, Andrea (ed.) et al., Financial cryptography and data security. FC 2019 international workshops, VOTING and WTSC, St. Kitts, St. Kitts and Nevis, February 18–22, 2019, Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 11599, 138-153 (2020). MSC: 91G99 94A60 91-04 PDFBibTeX XMLCite \textit{S. Crafa} et al., Lect. Notes Comput. Sci. 11599, 138--153 (2020; Zbl 1520.91442) Full Text: DOI
Downen, Paul; Ariola, Zena M.; Ghilezan, Silvia The duality of classical intersection and union types. (English) Zbl 1446.03034 Fundam. Inform. 170, No. 1-3, 39-92 (2019). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{P. Downen} et al., Fundam. Inform. 170, No. 1--3, 39--92 (2019; Zbl 1446.03034) Full Text: DOI
Audrito, Giorgio; Viroli, Mirko; Damiani, Ferruccio; Pianini, Danilo; Beal, Jacob A higher-order calculus of computational fields. (English) Zbl 1407.68326 ACM Trans. Comput. Log. 20, No. 1, Article No. 5, 55 p. (2019). MSC: 68Q85 PDFBibTeX XMLCite \textit{G. Audrito} et al., ACM Trans. Comput. Log. 20, No. 1, Article No. 5, 55 p. (2019; Zbl 1407.68326) Full Text: DOI arXiv
Docherty, Simon; Pym, David Intuitionistic layered graph logic: semantics and proof theory. (English) Zbl 1454.03030 Log. Methods Comput. Sci. 14, No. 4, Paper No. 11, 36 p. (2018). MSC: 03B47 03B20 03F03 PDFBibTeX XMLCite \textit{S. Docherty} and \textit{D. Pym}, Log. Methods Comput. Sci. 14, No. 4, Paper No. 11, 36 p. (2018; Zbl 1454.03030) Full Text: DOI arXiv
Jouannaud, Jean-Pierre; Strub, Pierre-Yves Coq without type casts: a complete proof of Coq Modulo Theory. (English) Zbl 1403.68227 Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 474-489 (2017). MSC: 68T15 PDFBibTeX XMLCite \textit{J.-P. Jouannaud} and \textit{P.-Y. Strub}, EPiC Ser. Comput. 46, 474--489 (2017; Zbl 1403.68227) Full Text: DOI
Amin, Nada; Rompf, Tiark Type soundness proofs with definitional interpreters. (English) Zbl 1380.68111 Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 666-679 (2017). MSC: 68N30 03B70 68T15 PDFBibTeX XMLCite \textit{N. Amin} and \textit{T. Rompf}, in: Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL '17, Paris, France, January 15--21, 2017. New York, NY: Association for Computing Machinery (ACM). 666--679 (2017; Zbl 1380.68111) Full Text: DOI
Chen, Tzu-Chun; Dezani-Ciancaglini, Mariangiola; Scalas, Alceste; Yoshida, Nobuko On the preciseness of subtyping in session types. (English) Zbl 1398.68360 Log. Methods Comput. Sci. 13, No. 2, Paper No. 12, 61 p. (2017). MSC: 68Q85 PDFBibTeX XMLCite \textit{T.-C. Chen} et al., Log. Methods Comput. Sci. 13, No. 2, Paper No. 12, 61 p. (2017; Zbl 1398.68360) Full Text: DOI arXiv
Lorenzen, Florian; Erdweg, Sebastian Sound type-dependent syntactic language extension. (English) Zbl 1347.68088 Bodik, Rastislav (ed.) et al., Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’16, St. Petersburg, FL, USA, January 20–22, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3549-2). 204-216 (2016). MSC: 68N30 68N15 68N20 PDFBibTeX XMLCite \textit{F. Lorenzen} and \textit{S. Erdweg}, in: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '16, St. Petersburg, FL, USA, January 20--22, 2016. New York, NY: Association for Computing Machinery (ACM). 204--216 (2016; Zbl 1347.68088) Full Text: DOI Link
Damiani, Ferruccio; Viroli, Mirko Type-based self-stabilisation for computational fields. (English) Zbl 1448.68336 Log. Methods Comput. Sci. 11, No. 4, Paper No. 21, 53 p. (2015). MSC: 68Q85 68N18 68Q55 PDFBibTeX XMLCite \textit{F. Damiani} and \textit{M. Viroli}, Log. Methods Comput. Sci. 11, No. 4, Paper No. 21, 53 p. (2015; Zbl 1448.68336) Full Text: DOI arXiv
Lorenzen, Florian; Erdweg, Sebastian Modular and automated type-soundness verification for language extensions. (English) Zbl 1323.68218 Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). ACM SIGPLAN Notices 48, No. 9, 331-342 (2013). MSC: 68N30 68N15 68N18 68Q60 PDFBibTeX XMLCite \textit{F. Lorenzen} and \textit{S. Erdweg}, in: Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP '13, Boston, MA, USA, September 25--27, 2013. New York, NY: Association for Computing Machinery (ACM). 331--342 (2013; Zbl 1323.68218) Full Text: DOI Link
Abed, Sa’ed; Mohamed, Otmane Ait; Al Sammane, Ghiath Automatic verification of reduction techniques in higher order logic. (English) Zbl 1298.68162 Formal Asp. Comput. 25, No. 6, 971-991 (2013). MSC: 68Q60 68T15 68T27 03B15 PDFBibTeX XMLCite \textit{S. Abed} et al., Formal Asp. Comput. 25, No. 6, 971--991 (2013; Zbl 1298.68162) Full Text: DOI
Swierstra, Wouter; Van Noort, Thomas A library for polymorphic dynamic typing. (English) Zbl 1286.68036 J. Funct. Program. 23, No. 3, 229-248 (2013). MSC: 68N15 68N18 PDFBibTeX XMLCite \textit{W. Swierstra} and \textit{T. Van Noort}, J. Funct. Program. 23, No. 3, 229--248 (2013; Zbl 1286.68036) Full Text: DOI
Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean Secure distributed programming with value-dependent types. (English) Zbl 1290.68033 J. Funct. Program. 23, No. 4, 402-451 (2013). MSC: 68N19 68N18 68N30 68N15 68T15 PDFBibTeX XMLCite \textit{N. Swamy} et al., J. Funct. Program. 23, No. 4, 402--451 (2013; Zbl 1290.68033) Full Text: DOI
Pottier, François Syntactic soundness proof of a type-and-capability system with hidden state. (English) Zbl 1262.68031 J. Funct. Program. 23, No. 1, 38-144 (2013). MSC: 68N18 03B70 68N30 PDFBibTeX XMLCite \textit{F. Pottier}, J. Funct. Program. 23, No. 1, 38--144 (2013; Zbl 1262.68031) Full Text: DOI
Meier, Martin An infinitary probability logic for type spaces. (English) Zbl 1276.91039 Isr. J. Math. 192, Part A, 1-58 (2012). Reviewer: Fernando Tohmé (Bahia Blanca) MSC: 91A44 91A10 62C10 03B42 03B48 91A26 PDFBibTeX XMLCite \textit{M. Meier}, Isr. J. Math. 192, Part A, 1--58 (2012; Zbl 1276.91039) Full Text: DOI
Rémy, Didier; Yakobowski, Boris A Church-style intermediate language for ML\(^{\text F}\). (English) Zbl 1252.03080 Theor. Comput. Sci. 435, 77-105 (2012). MSC: 03B70 03F52 68N18 68T15 PDFBibTeX XMLCite \textit{D. Rémy} and \textit{B. Yakobowski}, Theor. Comput. Sci. 435, 77--105 (2012; Zbl 1252.03080) Full Text: DOI
Ravara, António; Resende, Pedro; Vasconcelos, Vasco T. An algebra of behavioural types. (English) Zbl 1260.68277 Inf. Comput. 212, 64-91 (2012). Reviewer: Maciej Koutny (Newcastle upon Tyne) MSC: 68Q85 68Q60 68Q55 68N30 PDFBibTeX XMLCite \textit{A. Ravara} et al., Inf. Comput. 212, 64--91 (2012; Zbl 1260.68277) Full Text: DOI
Saabas, Ando; Uustalu, Tarmo Proof optimization for partial redundancy elimination. (English) Zbl 1187.68167 J. Log. Algebr. Program. 78, No. 7, 619-642 (2009). MSC: 68N99 PDFBibTeX XMLCite \textit{A. Saabas} and \textit{T. Uustalu}, J. Log. Algebr. Program. 78, No. 7, 619--642 (2009; Zbl 1187.68167) Full Text: DOI
Leroy, Xavier; Grall, Hervé Coinductive big-step operational semantics. (English) Zbl 1165.68044 Inf. Comput. 207, No. 2, 284-304 (2009). MSC: 68Q55 PDFBibTeX XMLCite \textit{X. Leroy} and \textit{H. Grall}, Inf. Comput. 207, No. 2, 284--304 (2009; Zbl 1165.68044) Full Text: DOI
Kamareddine, Fairouz; Nour, Karim A completeness result for a realisability semantics for an intersection type system. (English) Zbl 1127.03011 Ann. Pure Appl. Logic 146, No. 2-3, 180-198 (2007). Reviewer: Vladimir Komendantsky (Sophia Antipolis) MSC: 03B40 PDFBibTeX XMLCite \textit{F. Kamareddine} and \textit{K. Nour}, Ann. Pure Appl. Logic 146, No. 2--3, 180--198 (2007; Zbl 1127.03011) Full Text: DOI arXiv HAL
Johnsen, Einar Broch; Owe, Olaf; Yu, Ingrid Chieh Creol: A type-safe object-oriented model for distributed concurrent systems. (English) Zbl 1118.68031 Theor. Comput. Sci. 365, No. 1-2, 23-66 (2006). MSC: 68M14 PDFBibTeX XMLCite \textit{E. B. Johnsen} et al., Theor. Comput. Sci. 365, No. 1--2, 23--66 (2006; Zbl 1118.68031) Full Text: DOI
Bono, Viviana; Bugliesi, Michele; Dezani-Ciancaglini, Mariangiola; Liquori, Luigi A subtyping for extensible, incomplete objects. (English) Zbl 1040.03506 Fundam. Inform. 38, No. 4, 325-364 (1999). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{V. Bono} et al., Fundam. Inform. 38, No. 4, 325--364 (1999; Zbl 1040.03506)
Muñoz, César Dependent types with explicit substitutions: A meta-theoretical development. (English) Zbl 0927.03032 Giménez, Eduardo (ed.) et al., Types for proofs and programs. International workshop TYPES ’96, Aussois, France, December 15–19, 1996. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1512, 294-316 (1998). MSC: 03B40 PDFBibTeX XMLCite \textit{C. Muñoz}, Lect. Notes Comput. Sci. 1512, 294--316 (1998; Zbl 0927.03032)
Gallier, Jean Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus. (English) Zbl 0873.03017 Ann. Pure Appl. Logic 84, No. 3, 257-316 (1997). MSC: 03B40 18D15 03G30 PDFBibTeX XMLCite \textit{J. Gallier}, Ann. Pure Appl. Logic 84, No. 3, 257--316 (1997; Zbl 0873.03017) Full Text: DOI
Stefanova, M.; Geuvers, H. A simple model construction for the calculus of constructions. (English) Zbl 1434.03046 Berardi, Stefano (ed.) et al., Types for proofs and programs. International workshop TYPES ’95, Torino, Italy, June 5–8, 1995. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1158, 249-264 (1996). MSC: 03B38 03B40 03B70 PDFBibTeX XMLCite \textit{M. Stefanova} and \textit{H. Geuvers}, Lect. Notes Comput. Sci. 1158, 249--264 (1996; Zbl 1434.03046) Full Text: DOI Link
Geuvers, Herman A short and flexible proof of strong normalization for the calculus of constructions. (English) Zbl 07774797 Dybjer, Peter (ed.) et al., Types for proofs and programs. International workshop TYPES ’94, Båstad, Sweden, June 6–10, 1994. Selected papers. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 996, 14-38 (1995). MSC: 03B40 03B70 03F05 PDFBibTeX XMLCite \textit{H. Geuvers}, Lect. Notes Comput. Sci. 996, 14--38 (1995; Zbl 07774797) Full Text: DOI
Fisher, Kathleen; Honsell, Furio; Mitchell, John C. A lambda calculus of objects and method specialization. (English) Zbl 0886.03010 Nord. J. Comput. 1, No. 1, 3-37 (1994). MSC: 03B40 68N01 68N15 68Q55 03B70 PDFBibTeX XMLCite \textit{K. Fisher} et al., Nord. J. Comput. 1, No. 1, 3--37 (1994; Zbl 0886.03010)
Guzmán, Fernando A Gentzen system for conditional logic. (English) Zbl 0807.03011 Stud. Log. 53, No. 2, 243-257 (1994). Reviewer: T.Hosoi (Noda / Chiba) MSC: 03B50 PDFBibTeX XMLCite \textit{F. Guzmán}, Stud. Log. 53, No. 2, 243--257 (1994; Zbl 0807.03011) Full Text: DOI
Curien, Pierre-Louis; Ghelli, Giorgio Coherence of subsumption, minimum typing and type-checking in \(F_ \leq\). (English) Zbl 0765.03008 Math. Struct. Comput. Sci. 2, No. 1, 55-91 (1992). Reviewer: A.Pettorossi (Roma) MSC: 03B40 68Q55 PDFBibTeX XMLCite \textit{P.-L. Curien} and \textit{G. Ghelli}, Math. Struct. Comput. Sci. 2, No. 1, 55--91 (1992; Zbl 0765.03008) Full Text: DOI
Reyes, Gonzalo E. A topos-theoretic approach to reference and modality. (English) Zbl 0757.03013 Notre Dame J. Formal Logic 32, No. 3, 359-391 (1991). Reviewer: V.Shekhtman (Moskva) MSC: 03B65 03G30 03B45 18B25 PDFBibTeX XMLCite \textit{G. E. Reyes}, Notre Dame J. Formal Logic 32, No. 3, 359--391 (1991; Zbl 0757.03013) Full Text: DOI
Zbrzezny, Andrzej The Hilbert type axiomatization of some three-valued propositional logic. (English) Zbl 0721.03010 Z. Math. Logik Grundlagen Math. 36, No. 5, 415-421 (1990). Reviewer: A.Nakamura (Higashi-Hiroshima) MSC: 03B50 PDFBibTeX XMLCite \textit{A. Zbrzezny}, Z. Math. Logik Grundlagen Math. 36, No. 5, 415--421 (1990; Zbl 0721.03010) Full Text: DOI
Tofte, Mads Type inference for polymorphic references. (English) Zbl 0705.68028 Inf. Comput. 89, No. 1, 1-34 (1990). MSC: 68N15 68Q55 PDFBibTeX XMLCite \textit{M. Tofte}, Inf. Comput. 89, No. 1, 1--34 (1990; Zbl 0705.68028) Full Text: DOI
Dezani-Ciancaglini, Mariangiola; Margaria, Ines A characterization of F-complete type assignments. (English) Zbl 0619.03014 Theor. Comput. Sci. 45, 121-157 (1986). Reviewer: C.Masalagiu MSC: 03B40 03C65 68Q60 PDFBibTeX XMLCite \textit{M. Dezani-Ciancaglini} and \textit{I. Margaria}, Theor. Comput. Sci. 45, 121--157 (1986; Zbl 0619.03014) Full Text: DOI
Daniels, Charles B.; Freeman, James B. A logic of generalized quantification. (English) Zbl 0446.03008 Rep. Math. Logic 10, 9-42 (1978). MSC: 03B15 03C80 PDFBibTeX XMLCite \textit{C. B. Daniels} and \textit{J. B. Freeman}, Rep. Math. Logic 10, 9--42 (1978; Zbl 0446.03008)