## Volume XXIV, Issue 2, 2014

**Theoretical Aspects of Computing**, pages 173-176

We devote this issue of the Scientific Annals of Computer Science to the 11th International Colloquium on Theoretical Aspects of Computing. It contains the extended versions of five selected papers presented at ICTAC 2014 organized in Romania.

**DOI:** 10.7561/SACS.2014.2.173

[1] Gabriel Ciobanu and Dominique Méry (Editors). Proceedings of the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science, Springer, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7 .

**Probabilistic Recursion Theory and Implicit Computational Complexity**, pages 177-216

We show that probabilistic computable functions, i.e., those func- tions outputting distributions and computed by probabilistic Turing machines, can be characterized by a natural generalization of Church and Kleene’s partial recursive functions. The obtained algebra, following Leivant, can be restricted so as to capture the notion of a polytime sampleable distribution, a key concept in average-case complexity and cryptography.

**Keywords:** probabilistic recursion theory, implicit computational complexity, probabilistic Turing machines

**DOI:** 10.7561/SACS.2014.2.177

[1] Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the polytime functions. Computational complexity, 2(2):97–110, 1992. http://dx.doi.org/10.1007/BF01201998 .

[2] Andrej Bogdanov and Luca Trevisan. Average-case complexity. Foundations and Trends in Theoretical Computer Science, 2(1):1–106, 2006. http://dx.doi.org/10.1561/0400000004 .

[3] Dorin Comaniciu, Visvanathan Ramesh, and Peter Meer. Kernel-based object tracking. IEEE Transactions on Pattern Analysis and Machine Intelligence, 25(5):564–577, 2003. http://dx.doi.org/10.1109/TPAMI.2003.1195991 .

[4] Nigel J. Cutland. Computability: An introduction to recursive function theory. Cambridge University Press, 1980.

[5] Ugo Dal Lago and Paolo Parisen Toldin. A higher-order characterization of probabilistic polynomial time. In Ricardo Pen˜a, Marko C. J. D. van Eekelen, and Olha Shkaravska, editors, Foundational and Practical Aspects of Resource Analysis (FOPARA 2011), volume 7177 of Lecture Notes in Computer Science, pages 1–18. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-32495-6_1 .

[6] Ugo Dal Lago and Sara Zuppiroli. Probabilistic recursion theory and implicit computational complexity. In Gabriel Ciobanu and Dominique M´ery, editors, Proceedings of the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science, pages 97–114. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7_7 .

[7] Karel De Leeuw, Edward F Moore, Claude E Shannon, and Norman Shapiro. Computability by probabilistic machines. Automata studies, 34:183–198, 1956. http://dx.doi.org/10.1109/9780470544242.ch54 .

[8] John Gill. Computational complexity of probabilistic Turing ma- chines. SIAM Journal on Computing, 6(4):675–695, 1977. http://dx.doi.org/10.1137/0206049 .

[9] Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175–204, 1998. http://dx.doi.org/10.1006/inco.1998.2700 .

[10] Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of computer and system sciences, 28(2):270–299, 1984. http://dx.doi.org/10.1016/0022-0000(84)90070-9 .

[11] Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptogra- phy. Chapman and Hall/CRC Press, 2007.

[12] Stephen C. Kleene. General recursive functions of natural num- bers. Mathematische Annalen, 112(1):727–742, 1936. http://dx.doi.org/10.1007/bf01565439 .

[13] Daniel Leivant. Ramified recurrence and computational complex- ity I: Word recurrence and poly-time. In Peter Clote and Jef- freyB. Remmel, editors, Feasible Mathematics II, Progress in Com- puter Science and Applied Logic, pages 320–343. Springer, 1995. http://dx.doi.org/10.1007/978-1-4612-2566-9_11 .

[14] Daniel Leivant and Jean-Yves Marion. Lambda calculus characteriza- tions of poly-time. Fundamenta Informaticae, 19(1-2):167–184, 1993. http://dx.doi.org/10.1007/bfb0037112 .

[15] Christopher D. Manning and Hinrich Schu¨tze. Foundations of statistical natural language processing, volume 999. MIT Press, 1999.

[16] Judea Pearl. Probabilistic reasoning in intelligent systems: networks of plausible inference. Morgan Kaufmann, 1988.

[17] Michael O. Rabin. Probabilistic automata. Information and control, 6(3):230–245, 1963. http://dx.doi.org/10.1016/s0019-9958(63)90290-0 .

[18] Michael O. Rabin and Dana Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3(2):114–125, 1959. http://dx.doi.org/10.1147/rd.32.0114 .

[19] Eugene S. Santos. Probabilistic Turing machines and computability. Proceedings of the American Mathematical Society, 22(3):704–710, 1969. http://dx.doi.org/10.1090/s0002-9939-1969-0249221-4 .

[20] Eugene S. Santos. Computability by probabilistic Turing machines. Transactions of the American Mathematical Society, 159:165–184, 1971. http://dx.doi.org/10.2307/1996005 .

[21] Robert I. Soare. Recursively enumerable sets and degrees: a study of computable functions and computably generated sets. Perspectives in mathematical logic. Springer, 1987.

[22] Sebastian Thrun. Robotic mapping: A survey. In Gerhard Lakemeyer and Bernhard Nebel, editors, Exploring Artificial Intelligence in the New Millennium, pages 1–35. Morgan Kaufmann Publishers Inc., 2003.

**Rely-Guarantee Based Reasoning for Message-Passing Programs**, pages 217-252

The difficulties of verifying concurrent programs lie in their inherent non-determinism and interferences. Rely-Guarantee reasoning is one useful approach to solve this problem for its capability in formally specifying inter- thread interferences. However, modern verification requires better locality and modularity. It is still a great challenge to verify a message-passing program in a modular and composable way. In this paper, we propose a new reasoning system for message-passing programs. It is a novel logic that supports Hoare style triples to specify and verify distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and specify behav- iors of agents by their local traces with regard to environmental assumptions — an idea inspired by Rely-Guarantee reasoning. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. To show validity, we apply our logic to modularly prove several examples.

**Keywords:** trace semantics, message passing, rely guarantee

**DOI:** 10.7561/SACS.2014.2.217

[1] Mark Bickford and Robert L. Constable. A causal logic of events in formalized computational type theory. Technical report, Cornell University, 2005.

[2] Stephen D. Brookes. A semantics for concurrent separation logic. In Philippa Gardner and Nobuko Yoshida, editors, Proceedings of the 15th International Conference on Concurrency Theory (CONCUR 2004), volume 3170 of Lecture Notes in Computer Science, pages 16–34. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-28644-8_2 .

[3] Bernadette Charron-Bost, Friedemann Mattern, and Gerard Tel. Synchronous, asynchronous, and causally ordered communication. Distributed Computing, 9(4):173–191, 1996. http://dx.doi.org/10.1007/s004460050018 .

[4] Willem-Paul de Roever, Frank de Boer, Ulrich Hanneman, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. Concurrency Verifica- tion: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, January 2012.

[5] Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkin- son, and Viktor Vafeiadis. Concurrent abstract predicates. In Theo D’Hondt, editor, Proceedings of the 24th European Conference on Object- Oriented Programming (ECOOP 2010), volume 6183 of Lecture Notes in Computer Science, pages 504–528. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-14107-2_24 .

[6] Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Rocco De Nicola, editor, Proceedings of the 16th European Symposium on Programming (ESOP 2007), volume 4421 of Lecture Notes in Computer Science, pages 173–188. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-71316-6_13 .

[7] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978. http://dx.doi.org/10.1145/359576.359585 .

[8] Cliff B. Jones. Tentative steps toward a development method for interfer- ing programs. ACM Transactions on Programming Languages and System, 5(4):596–619, 1983. http://dx.doi.org/10.1145/69575.69577 .

[9] Gilles Kahn. The semantics of simple language for parallel programming. In IFIP Congress, pages 471–475, 1974.

[10] Leslie Lamport. Time, clocks, and the ordering of events in a distributed sys- tem. Communications of the ACM, 21(7):558–565, 1978. http://dx.doi.org/10.1145/359545.359563 .

[11] Jinjiang Lei and Zongyan Qiu. Modular reasoning for message-passing programs. In Gabriel Ciobanu and Dominique Me´ry, editors, Proceedings of the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science, pages 277–294. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7_17 .

[12] Jinjiang Lei and Zongyan Qiu. Modular reasoning for message-passing programs. Technical report, School of Mathematical Sciences, Peking Univer- sity, Sep 2014. Available from: hhttps://sites.google.com/site/jinjianglei/publications/rgdsep_journal.

[13] Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. http://dx.doi.org/10.1007/3-540-10235-3 .

[14] RRobin Milner. Communication and Concurrency. PHI Series in computer science. Prentice Hall, 1989.

[15] Robin Milner. The polyadic pi-calculus (abstract). In Rance Cleaveland, editor, Proceedings of the Third International Conference on Concurrency Theory (CONCUR 1992), volume 630 of Lecture Notes in Computer Science, page 1. Springer, 1992. http://dx.doi.org/10.1007/BFb0084778 .

[16] Robin Milner. Communicating and mobile systems - the Pi-calculus. Cam- bridge University Press, 1999.

[17] Matthew J. Parkinson, Richard Bornat, and Cristiano Calcagno. Variables as resource in Hoare logics. In Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pages 137–146. IEEE Computer Society, 2006. http://dx.doi.org/10.1109/LICS.2006.52 .

[18] Uday S. Reddy and John C. Reynolds. Syntactic control of interference for separation logic. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pages 323–336. ACM, 2012. http://dx.doi.org/10.1145/2103656.2103695 .

[19] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pages 55–74. IEEE Computer Society, 2002. http://dx.doi.org/10.1109/LICS.2002.1029817 .

[20] Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely/guarantee and separation logic. In Luís Caires and Vasco Thudichum Vasconcelos, editors, Proceedings of the 18th International Conference on Concurrency Theory (CONCUR 2007), volume 4703 of Lecture Notes in Computer Science, pages 256–271. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-74407-8_18 .

[21] Jules Villard, Étienne Lozes, and Cristiano Calcagno. Proving copyless message passing. In Zhenjiang Hu, editor, Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS'09), volume 5904 of Lecture Notes in Computer Science, pages 194–209. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-10672-9_15 .

[22] Ian Wehrman, C. A. R. Hoare, and Peter W. O’Hearn. Graphical models of separation logic. Information Processing Letters, 109(17):1001–1004, 2009. http://dx.doi.org/10.1016/j.ipl.2009.06.003 .

**Learning Cover Context-Free Grammars from Structural Data**, pages 253-286

We consider the problem of learning an unknown context-free gram- mar from its structural descriptions with depth at most ℓ. The structural descriptions of the context-free grammar are its unlabelled derivation trees. The goal is to learn a *cover context-free grammar* (CCFG) with respect to ℓ, that is, a CFG whose structural descriptions with depth at most ℓ agree with those of the unknown CFG. We propose an algorithm, called *LA*^{ℓ}, that efficiently learns a CCFG using two types of queries: structural equivalence and structural membership. The learning proto- col is based on what is called in the literature a "minimally adequate teacher." We show that *LA*^{ℓ} runs in time polynomial in the number of states of a minimal deterministic finite cover tree automaton (DCTA) with respect to ℓ. This number is often much smaller than the number of states of a minimum deterministic finite tree automaton for the structural descriptions of the unknown grammar.

**Keywords:** automata theory and formal languages, grammatical inference, structural descriptions

**DOI:** 10.7561/SACS.2014.2.253

[1] Dana Angluin. Learning regular sets from queries and counterex- amples. Information and Computation, 75(2):87–106, 1987. http://dx.doi.org/10.1016/0890-5401(87)90052-6 .

[2] Dana Angluin and Michael Kharitonov. When won’t membership queries help? Journal of Computer and System Sciences, 50(2):336–355, 1995. http://dx.doi.org/10.1006/jcss.1995.1026 .

[3] Walter S. Brainerd. The minimalization of tree automata. Informa- tion and Control, 13(5):484–491, 1968. http://dx.doi.org/10.1016/S0019-9958(68)90917-0 .

[4] Cezar Câmpeanu, Nicolae Sântean, and Sheng Yu. Minimal cover- automata for finite languages. Theoretical Computer Science, 267(1– 2):3–16, 2001. Workshop on Implementing Automata '98. http://dx.doi.org/10.1016/S0304-3975(00)00292-9.

[5] Colin De la Higuera. Grammatical inference: Learning automata and Grammars. Cambridge University Press, 2010.

[6] Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, and Bow-Yaw Wang. Extending automated compositional verification to the full class of omega-regular languages. In C. R. Ramakrishnan and Jakob Rehof, editors, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2008), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2008), volume 4963 of Lecture Notes in Computer Science, pages 2–17. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-78800-3_2 .

[7] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Pearson Addison Wesley, second edition, 2003.

[8] Florentin Ipate. Learning finite cover automata from queries. Journal of Computer and System Sciences, 78(1):221–244, 2012. http://dx.doi.org/10.1016/j.jcss.2011.04.002 .

[9] Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan. Minimization, learning, and conformance testing of boolean programs. In Christel Baier and Holger Hermanns, editors, Proceedings of the 17th International Conference on Concurrency Theory (CONCUR 2006), volume 4137 of Lecture Notes in Computer Science, pages 203–217. Springer, 2006. http://dx.doi.org/10.1007/11817949_14 .

[10] Leon S. Levy and Aravind K. Joshi. Skeletal structural descrip- tions. Information and Control, 39(2):192–211, 1978. http://dx.doi.org/10.1016/S0019-9958(78)90849-5 .

[11] Oded Maler and Amir Pnueli. On the learnability of infinitary regular sets. Information and Computation, 118(2):316–326, 1995. http://dx.doi.org/10.1006/inco.1995.1070 .

[12] Yasubumi Sakakibara. Learning context-free grammars from structural data in polynomial time. Theoretical Computer Science, 76(2-3):223–242, 1990. http://dx.doi.org/10.1016/0304-3975(90)90017-C .

[13] Michael Sipser. Introduction to the Theory of Computation. Thomson, 2nd edition, 2006.

**Arithmetic and Boolean Operations on Recursively Run-Length Compressed Natural Numbers**, pages 287-323

We study arithmetic properties of a new tree-based canonical num- ber representation, *recursively run-length compressed* natural numbers, defined by applying recursively a run-length encoding of their binary digits.
We design arithmetic and boolean operations with recursively run- length compressed natural numbers that work a block of digits at a time and are limited only by the representation complexity of their operands, rather than their bitsizes.
As a result, operations on very large numbers exhibiting a regular structure become tractable.
In addition, we ensure that the average complexity of our operations is still within constant factors of the usual arithmetic operations on binary numbers.
Arithmetic operations on our recursively run-length compressed are specified as pattern-directed recursive equations made executable by using a purely declarative subset of the functional language Haskell.

**Keywords:** run-length compressed numbers, hereditary numbering systems, arithmetic algorithms for giant numbers, representation com- plexity of natural numbers

**DOI:** 10.7561/SACS.2014.2.287

[1] J. W. Bruce. A Really Trivial Proof of the Lucas-Lehmer Test. The American Mathematical Monthly, 100(4):370–371, 1993. http://dx.doi.org/10.2307/2324959.

[2] John H. Conway. On Numbers and Games. AK Peters, Ltd., 2nd edition, 2000.

[3] R. Goodstein. On the restricted ordinal theorem. Journal of Symbolic Logic, 9(02):33–41, 1944. http://dx.doi.org/10.2307/2268019 .

[4] Norbert Hungerbühler. The Isomorphism Problem for Catalan Families. J. Combin. Inform. System Sci, 20:129–139, 1995.

[5] Oleg Kiselyov, William E. Byrd, Daniel P. Friedman, and Chung- chieh Shan. Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl). In Jacques Garrigue and Manuel V. Hermenegildo, editors, Proceedings of the 9th International Symposium on Functional and Logic Programming (FLOPS 2008), volume 4989 of Lecture Notes in Computer Science, pages 64–80. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-78969-7_7 .

[6] Donald E. Knuth. Mathematics and Computer Science: Coping with Finiteness. Science, 194c;4271):1235 –1242, 1976. http://dx.doi.org/10.1126/science.194.4271.1235 .

[7] Donald E. Knuth. TCALC program, December 1994. http://www-cs-faculty.stanford.edu/~uno/programs/tcalc.w.gz .

[8] Donald E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 4: Generating All Trees–History of Combinatorial Generation (Art of Computer Programming). Addison-Wesley Professional, 2006.

[9] Donald E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams. Addison-Wesley Professional, 2009.

[10] Donald L. Kreher and D.R. Stinson. Combinatorial Algorithms: Generation, Enumeration, and Search. The CRC Press Series on Discrete Mathematics and its Applications. CRC Press, 1999.

[11] Ming Li and Paul Vit´anyi. An introduction to Kolmogorov complexity and its applications. Springer-Verlag New York, Inc., New York, NY, USA, 1993.

[12] J. Liebehenschel. Ranking and unranking of a generalized Dyck language and the application to the generation of random trees. Séminaire Lotharingien de Combinatoire, 43:B43d, 19 p.–B43d, 19 p., 1999. Available from: http://eudml.org/doc/120437 .

[13] Conrado Martìnez and Xavier Molinero. Generic algorithms for the generation of combinatorial objects. In Branislav Rovan and Peter Vojtás, editors, Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS 2003), volume 2747 of Lecture Notes in Computer Science, pages 572–581. Springer, 2003. http://dx.doi.org/10.1007/978-3-540-45138-9_51.

[14] Arto Salomaa. Formal Languages. Academic Press, New York, 1973.

[15] R P Stanley. Enumerative Combinatorics. Wadsworth Publ. Co., Belmont, CA, USA, 1986.

[16] Paul Tarau. Declarative modeling of finite mathematics. In Temur Kutsia, Wolfgang Schreiner, and Maribel Fernández, editors, Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2010), pages 131–142. ACM, 2010. http://dx.doi.org/10.1145/1836089.1836107 .

[17] Paul Tarau. Computing with Catalan Families. In Adrian Horia Dediu, Carlos Martìn-Vide, José Luis Sierra-Rodríguez, and Bianca Truthe, editors, Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014), volume 8370 of Lecture Notes in Computer Science, pages 565–575. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-04921-2_46 .

[18] Paul Tarau. The Arithmetic of Recursively Run-Length Compressed Natural Numbers. In Gabriel Ciobanu and Dominique Méry, editors, Proceedings of the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science, pages 406–423. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7_24 .

[19] Paul Tarau and Bill P. Buckles. Arithmetic algorithms for hereditarily binary natural numbers. In Yookun Cho, Sung Y. Shin, Sang-Wook Kim, Chih-Cheng Hung, and Jiman Hong, editors, Proceedings of the Symposium on Applied Computing (SAC 2014), pages 1593–1600. ACM, 2014. http://dx.doi.org/10.1145/2554850.2555040 .

[20] Paul Tarau and David Haraburda. On computing with types. In Sascha Ossowski and Paola Lecca, editors, Proceedings of the ACM Symposium on Applied Computing (SAC 2012), pages 1889–1896. ACM, 2012. http://dx.doi.org/10.1145/2245276.2232087 .

[21] Paul Tarau and Brenda Luderman. Boolean evaluation with a pairing and unpairing function. In Andrei Voronkov, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen Watt, and Daniela Zaharie, editors, Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), pages 384–390. IEEE Computer Society. http://dx.doi.org/10.1109/SYNASC.2012.20 .

[22] Jean Vuillemin. Efficient data structure and algorithms for sparse integers, sets and predicates. In Javier D. Bruguera, Marius Cornea, Debjit Das Sarma, and John Harrison, editors, Proceedings of the 19th IEEE Symposium on Computer Arithmetic (ARITH 2009), pages 7–14. IEEE Computer Society, 2009. http://dx.doi.org/10.1109/ARITH.2009.25 .

**Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces**, pages 325-368

In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language, while the second model is not. We then develop an algebraic extension of the finite lambda calculus and study two operational semantics: a call-by-name and a call-by-value. These operational semantics are matched with their corresponding natural denotational semantics based on finite vector spaces. The relationship between the various semantics is analyzed, and several examples based on Church numerals are presented.

**Keywords:** Finite vector spaces, finite sets, algebraic lambda-calculus, Kleisli category, Eilenberg-Moore category.

**DOI:** 10.7561/SACS.2014.2.325

[1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, Vol. 163, pp. 409–470, 2000. http://dx.doi.org/10.1006/inco.2000.2930 .

[2] P. Arrighi, A. Díaz-Caro, and B. Valiron. A type system for the vectorial aspects of the linear-algebraic lambda-calculus. In Proceedings of the 7th International Workshop on Developments of Computational Methods (DCM 2011), Electronic Proceedings in Theoretical Computer Science, Vol. 88, pp. 1–15, 2012. http://dx.doi.org/10.4204/EPTCS.88.1 .

[3] P. Arrighi and A. Díaz Caro. A System F accounting for scalars. Logic Methods in Computer Science, Vol. 8, Paper 11, 2012. http://dx.doi.org/10.2168/LMCS-8(1:11)2012 .

[4] P. Arrighi and G. Dowek. Linear-algebraic λ-calculus: higher-order, encodings, and confluence. In Proceedings of the 19th international conference on Rewriting Techniques and Applications (RTA ’08), Lec- ture Notes in Computer Science, Vol. 5117, pp. 17–31, 2008. http://dx.doi.org/10.1007/978-3-540-70590-1_2 .

[5] N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proceedings of the 8th Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 933, pp 121–135, 1995. http://dx.doi.org/10.1007/BFb0022251 .

[6] G. Bierman. On Intuitionistic Linear Logic. PhD thesis, Cambridge Univ., 1994. Also Tech. Report UCAM-CL-TR-346.

[7] A. Bucciarelli, T. Ehrhard, and G. Manzonetto. A relational semantics for parallelism and non-determinism in a functional setting. Ann. Annals of Pure and Applied Logic, Vol. 163, pp. 918–934, 2012. http://dx.doi.org/10.1016/j.apal.2011.09.008 .

[8] P. de Groote. Strong normalization in a non-deterministic typed lambda-calculus. In Proceedings of the Third International Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 813, pp. 142–152, 1994. http://dx.doi.org/10.1007/3-540-58140-5_15 .

[9] A. Díaz-Caro. Du Typage Vectoriel. PhD thesis, Univ. de Grenoble, 2011. Archived online at tel.archives-ouvertes.fr:tel-00631514.

[10] T. Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, Vol. 15, pp. 615–646, 2005. http://dx.doi.org/10.1017/S0960129504004645 .

[11] T. Ehrhard, M. Pagani, and C. Tasson. The computational meaning of probabilistic coherence spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011), pp. 87–96, 2011. http://dx.doi.org/10.1109/LICS.2011.29 .

[12] T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, Vol. 309, pp. 1–41, 2003. http://dx.doi.org/10.1016/S0304-3975(03)00392-X .

[13] J.-Y. Girard. Linear logic. Theoretical Computer Science, Vol. 50, pp. 1–101, 1987. http://dx.doi.org/10.1016/0304-3975(87)90045-4 .

[14] J.-Y. Girard, A. Scedrov and P. J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theoretical Com- puter Science, Vol. 97, pp. 1–65, 1992. http://dx.doi.org/10.1016/0304-3975(92)90386-T .

[15] J.-Y. Girard, Y. Lafont, and P. Taylor. Proof and Types. Cambridge Univ. Press, 1990. Available online at http://www.paultaylor.eu/stable/Proofs%2BTypes.html .

[16] G. G. Hillebrand. Finite Model Theory in the Simply Typed Lambda Calculus. PhD thesis, Brown Univ., 1991. Also Tech. Report CS-94-24.

[17] M. Hyland and A. Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, Vol. 294, pp. 183–231, 2003. http://dx.doi.org/10.1016/S0304-3975(01)00241-9 .

[18] R. P. James, G. Ortiz, and A. Sabry. Quantum computing over finite fields. Draft, 2011. Found on http://arxiv.org/abs/1101.3764 .

[19] J. Lambek and P. J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge Univ. Press, 1994.

[20] S. Lang. Algebra. Springer, 2005.

[21] R. Lidl. Finite fields, Cambridge Univ. Press, 1997.

[22] S. Mac Lane. Categories for the Working Mathematician. Springer, 1998.

[23] R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, Vol. 4, pp. 1–22, 1977. http://dx.doi.org/10.1016/0304-3975(77)90053-6 .

[24] G. Plotkin. LCF considered as a programming language. Theoret- ical Computer Science, Vol. 5, pp. 223–255, 1977. http://dx.doi.org/10.1016/0304-3975(77)90044-5 .

[25] V. R. Pratt. Re: Linear logic semantics (barwise). On the TYPES mailing list, February 1992. http://www.seas.upenn.edu/~sweirich/types/archive/1992/msg00047.html .

[26] V. R. Pratt. Chu spaces: Complementarity and uncertainty in rational mechanics. Technical report, Stanford Univ., 1994. Course notes, TEMPUS summer school, 35 pages. http://boole.stanford.edu/pub/bud.pdf .

[27] S. Salvati. Recognizability in the simply typed lambda-calculus. In Pro- ceedings of 16th International Workshop on Logic, Language, Informa- tion and Computation (WoLLIC 2009), Lecture Notes in Computer Sci- ence, Vol. 5514, pp. 48–60, 2009. http://dx.doi.org/10.1007/978-3-642-02261-6_5 .

[28] B. Schumacher and M. D. Westmoreland. Modal quantum theory. In Proceedings of the 7th Workshop on Quantum Physics and Logic, pp. 145–149, 2010. http://www.cs.ox.ac.uk/people/bob.coecke/QPL_proceedings.html .

[29] D. S. Scott. A type-theoretic alternative to CUCH, ISWIM, OWHY. Theoretical Computer Science, Vol. 121, pp. 411–440, 1993. http://dx.doi.org/10.1016/0304-3975(93)90095-B .

[30] P. Selinger. Order-incompleteness and finite lambda reduction models. Theoretical Computer Science, Vol. 309, pp. 43–63, 2003. http://dx.doi.org/10.1016/S0304-3975(02)00038-5 .

[31] S. Soloviev. Category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, Vol. 22, pp. 1387–1400, 1983. http://dx.doi.org/10.1007/BF01084396 .

[32] B. Valiron. A typed, algebraic, computational lambda-calculus. Math- ematical Structures in Computer Science, Vol. 23, pp. 504–554, 2013. http://dx.doi.org/10.1017/S0960129512000205 .

[33] B. Valiron and S. Zdancewic. Finite vector spaces as model of simply-typed lambda-calculi. In Proceedings of the 11th Interna- tional Colloquium on Theoretical Aspects of Computing (ICTAC 2014), Lecture Notes in Computer Science, Vol. 8687, pp. 442–459, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7_26 .

[34] L. Vaux. The algebraic lambda-calculus. Mathematical Structures in Computer Science, Vol. 19, pp. 1029–1059, 2009. http://dx.doi.org/10.1017/S0960129509990089 .

[35] G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.