Nissim Francez

Nissim Francez (Hebrew: נסים פרנסיז; born 19 January 1944 in Bulgaria) is an Israeli professor, emeritus in the computer science faculty at the Technion, and former head of computational linguistics laboratory in the faculty.^[1]

He received his B.Sc. in mathematics and philosophy from the Hebrew University, Jerusalem in 1965. After his military service in the Israel Defense Forces, he studied at the Department of Applied Mathematics at the Weizmann Institute, Rehovot, and received his M.sc. in 1971.

He continued his studies there and received his Ph.D. degree in 1976 under the supervision of Prof. Amir Pnueli.^[2]

In 1991 he became a full professor at the Computer Science Faculty in the Technion, and from 1996 to 2006 he was the head of the Computational Linguistics Laboratory at the faculty. Francez held the Bank Leumi chair in Computer Science in the faculty from 2000 until 2010, when he retired from the Technion as professor emeritus.^[2]

Francez was working in IBM Scientific Center, Haifa in 1981 to 1982, and a year later at IBM-T.J.Watson Research Center, Yorktown Heights, New York, United States as a visiting scientist. In 1983-85 he was working on design and implementation of a Prolog programming environment at IBM Scientific Center, Haifa. He was a visiting scientist at Microelectronics and Computer Technology Corporation (MCC), Austin, Texas, US in the summers of 1986 and 1987 and 1989-1990 In 1997 he was a visiting scientist at Centrum Wiskunde & Informatica (CWI), Amsterdam.^[2]

He was also a Guest Editor (with Ian Pratt-Hartmann) of a special issue of Studia Logica Logic and Natural Language, 2012.^[3]

In his sabbaticals and summer leaves, Francez has been a research associate at Aiken Computation Lab. at Harvard University in the summers of 1981 and 1982. He was also a visiting scientist at Abo Academy, Turku, Finland (1988) and at the Department of Computer Science, University of Utrecht, The Netherlands (1992). Francez was an Honorary Visiting Professor at the Department of CS, Manchester University (1996-1997), and a Senior Academic Visitor at HCRC, Department of Informatics, Edinburgh University (2002)^[4] and at the School of Computer Science, St Andrews University (2007).^[2]

Francez’s research spans theoretical computer science , formal logic, and computational linguistics.^[5]

Francez’s initial research focused on the semantics of programming languages, program verification, and concurrency theory.^[6][2] He introduced rigorous formalizations of fairness in concurrent systems, developing methods for reasoning about scheduling, liveness, and nondeterminism in distributed programs. His influential monograph Fairness (1986)^[7] and the textbook Program Verification (1992) provided systematic treatments of methods and tools for proving program correctness, including for concurrent and distributed systems. ^[8]In this period, he also contributed to logic programming and published on the direct verification of program properties, such as in Acta Informatica (1983).^[9]

In the 1990s, Francez extended his research into computational linguistics, focusing on the formal representation of natural language syntax and semantics.^[10] He worked with unification-based grammar formalisms, including Lexical Functional Grammar (LFG) and Head-Driven Phrase Structure Grammar (HPSG), contributing to their theoretical foundations and linguistic applications.

Since the early 2000s, Francez has been a leading figure in the development of proof-theoretic semantics, an alternative to truth-conditional semantics that defines meaning through inference rules. He applied proof-theoretic semantics to natural language phenomena such as quantifier scope ambiguity, adjectival modification, domain restriction, omitted arguments, and contexts blocking entailment.^[4] His work introduced the notion of bilateralism, extending proof systems to treat assertion and denial symmetrically, and developed proof-theoretic semantic values for logical operators.^[11]

In parallel, he contributed to type-logical grammar, exploring how function–argument structures can be used to assign semantic values compositionally, in line with Frege’s Context Principle. This approach emphasized meaning as determined by introduction rules in natural deduction rather than by model-theoretic semantics.^[12]

His co-authored book with Shuly Wintner, Unification Grammars (2011), offered a mathematically rigorous introduction to the field and has been widely cited.^[13]

In more recent years, Francez has devoted considerable attention to connexive logics, a non-classical family of logical systems that reject paradoxes of implication in classical logic, such as the principle that “if not-A, then A implies B.” ^[14]His work develops proof-theoretic foundations for connexive reasoning, aligning with his broader program of defining meaning through inference rules. This line of research culminated in his book A View of Connexive Logics (2021), which offers a systematic exposition of the field, situates connexive principles within the history of logic, and explores their relevance for both philosophical and computational applications.^[15]

• Francez, Nissim (1986). Fairness. Monographs in Computer Science Ser. New York, NY: Springer New York. ISBN 978-1-4612-4886-6.
• Francez, Nissim (1992). Program Verification. Addison-Wesley Publishing Company. ISBN 978-0-201-41608-4.
• Francez, Nissim; Forman, Ira R. (1996). Interacting Processes: A Multiparty Approach to Coordinated Distributed Programming. Addison-Wesley. ISBN 978-0-201-56528-7.
• Francez, Nissim; Wintner, Shuly (2011). Unification Grammars. Cambridge University Press. ISBN 978-1-139-50357-0.
• Francez, Nissim (2012). Fairness. Springer Science & Business Media. ISBN 978-1-4612-4886-6.
• Francez, Nissim (2015). Proof-theoretic Semantics. College Publications. ISBN 978-1-84890-183-4.
• Francez, Nissim (2021). A View of Connexive Logics. College Publications. ISBN 9781848903708.

• Francez, Nissim; Pnueli, Amir (1 June 1978). "A proof method for cyclic programs". Acta Informatica. 9 (2): 133–157. doi:10.1007/BF00289074. ISSN 1432-0525. S2CID 40233148.
• Francez, Nissim; Hoare, C.A.R.; Lehmann, Daniel J.; De Roever, Willem P. (December 1979). "Semantics of nondeterminism, concurrency, and communication". Journal of Computer and System Sciences. 19 (3): 290–308. doi:10.1016/0022-0000(79)90006-0. ISSN 0022-0000.
• Apt, Krzysztof R.; Francez, Nissim; de Roever, Willem P. (July 1980). "A Proof System for Communicating Sequential Processes". ACM Transactions on Programming Languages and Systems. 2 (3): 359–385. doi:10.1145/357103.357110. ISSN 0164-0925.
• Francez, Nissim (January 1980). "Distributed Termination". ACM Transactions on Programming Languages and Systems. 2 (1): 42–55. doi:10.1145/357084.357087. ISSN 0164-0925.
• Francez, N.; Rodeh, M. (May 1982). "Achieving Distributed Termination without Freezing". IEEE Transactions on Software Engineering. SE-8 (3): 287–292. Bibcode:1982ITSEn...8..287F. doi:10.1109/tse.1982.235257. ISSN 0098-5589.
• Elrad, Tzilla; Francez, Nissim (December 1982). "Decomposition of distributed programs into communication-closed layers". Science of Computer Programming. 2 (3): 155–173. doi:10.1016/0167-6423(83)90013-8. ISSN 0167-6423.
• Francez, N.; Lehmann, D.; Pnueli, A. (1984). "A linear-history semantics for languages for distributed programming". Theoretical Computer Science. 32 (1–2): 25–46. doi:10.1016/0304-3975(84)90022-7. ISSN 0304-3975.
• Grumberg, Orna; Francez, Nissim; Makowsky, Johann A.; de Roever, Willem P. (1 July 1985). "A proof rule for fair termination of guarded commands". Information and Control. 66 (1): 83–102. doi:10.1016/S0019-9958(85)80014-0. ISSN 0019-9958.
• Francez, Nissim; Hailpern, Brent; Taubenfeld, Gadi (1986). "Script: A communication abstraction mechanism and its verification". Science of Computer Programming. 6: 35–88. doi:10.1016/0167-6423(86)90018-3. ISSN 0167-6423.
• Apt, Krzysztof R.; Francez, Nissim; Katz, Shmuel (1988). "Appraising fairness in languages for distributed programming". Distributed Computing. 2 (4): 226–241. doi:10.1007/bf01872848. ISSN 0178-2770.
• Bougé, L.; Francez, N. (1988). "A compositional approach to superimposition". Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '88. New York, New York, USA: ACM Press. pp. 240–249. doi:10.1145/73560.73581. ISBN 0-89791-252-7.
• Couvreur, J.-M.; Francez, N.; Gouda, M. (1992). "Asynchronous unison". [1992] Proceedings of the 12th International Conference on Distributed Computing Systems. IEE Compt. Soc. Press. pp. 486–493. doi:10.1109/icdcs.1992.235005. ISBN 0-8186-2865-0.
• Lappin, Shalom; Francez, Nissim (August 1994). "E-type pronouns, i-sums, and donkey anaphora". Linguistics and Philosophy. 17 (4): 391–428. doi:10.1007/bf00985574. ISSN 0165-0157.
• Pratt, Ian; Francez, Nissim (April 2001). "Temporal Prepositions and Temporal Generalized Quantifiers". Linguistics and Philosophy. 24 (2): 187–222. doi:10.1023/a:1005632801858. ISSN 0165-0157.
• Francez, Nissim; Dyckhoff, Roy (December 2010). "Proof-theoretic semantics for a natural language fragment". Linguistics and Philosophy. 33 (6): 447–477. doi:10.1007/s10988-011-9088-3. ISSN 0165-0157.
• Francez, Nissim (2021). "Proof-Theoretic Semantics for Natural Language". Topoi. 40 (1): 55–69. doi:10.1007/s11245-019-09662-5. ISSN 0167-7411.

• Nissim Francez, Google Scholar
• Nissim Francez at the Mathematics Genealogy Project
• Nissim Francez, at DBLP Bibliography Server