{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:06:29Z","timestamp":1761620789101,"version":"3.43.0"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2000,8,1]],"date-time":"2000-08-01T00:00:00Z","timestamp":965088000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,8,1]],"date-time":"2000-08-01T00:00:00Z","timestamp":965088000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,8]]},"DOI":"10.1023\/a:1008780817617","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"5-37","source":"Crossref","is-referenced-by-count":4,"title":["Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic"],"prefix":"10.1007","volume":"17","author":[{"given":"Michael","family":"Mendler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"267091_CR1","volume-title":"International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems","author":"ACM, in","year":"1993","unstructured":"ACM, in International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Intermar Hotel Malente, Germany, September 1993."},{"key":"267091_CR2","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S. Akers","year":"1978","unstructured":"S. Akers, \"Binary decision diagrams,\u201d IEEE Transactions on Computers, Vol. C-27, pp. 509\u2013516, 1978.","journal-title":"IEEE Transactions on Computers"},{"key":"267091_CR3","unstructured":"D. Basin, \u201cExtracting circuits from constructive proofs,\u201d in Int'l Workshop on: Formal Methods for VLSI Design, Miami, USA, January 1991. IFIP-IEEE."},{"key":"267091_CR4","first-page":"31","volume":"939","author":"D. Basin","year":"1995","unstructured":"D. Basin and N. Klarlund, \u201cHardware verification using monadic second-order logic,\u201d in Proc. Computer Aided Verification CAV'95. LNCS, Vol. 939, Springer, 1995, pp. 31\u201341.","journal-title":"Proc. Computer Aided Verification CAV'95"},{"key":"267091_CR5","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/S0167-9260(83)80018-2","volume":"1","author":"J.A. Bergstra","year":"1983","unstructured":"J.A. Bergstra and J.W. Klop, \u201cA proof rule for restoring logic circuits,\u201d INTEGRATION, the VLSI Journal, Vol. 1, pp. 161\u2013178, 1983.","journal-title":"INTEGRATION, the VLSI Journal"},{"issue":"4","key":"267091_CR6","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1109\/TC.1972.5008985","volume":"C-21","author":"M.A. Breuer","year":"1972","unstructured":"M.A. Breuer, \u201cA note on three-valued logic simulation,\u201d IEEE Transactions on Computers, Vol. C-21, No. 4, pp. 399\u2013402, April 1972.","journal-title":"IEEE Transactions on Computers"},{"key":"267091_CR7","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, \u201cA switch-level model and simulator for MOS digital systems,\u201d IEEE Transactions on Computers, Vol. C-33, pp.160\u2013177, February 1984.","DOI":"10.1109\/TC.1984.1676408"},{"issue":"4","key":"267091_CR8","doi-asserted-by":"crossref","first-page":"634","DOI":"10.1109\/TCAD.1987.1270310","volume":"6","author":"R.E. Bryant","year":"1987","unstructured":"R.E. Bryant, \u201cBoolean analysis of MOS circuits,\u201d IEEE Transactions on Computer-Aided Design, Vol. 6, No.4, pp. 634\u2013649, July 1987.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"267091_CR9","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1109\/TC.1979.1675317","volume":"C-28","author":"J.A. Brzozowski","year":"1979","unstructured":"J.A. Brzozowski and M. Yoeli, \u201cOn a ternary model of gate networks,\u201d IEEE Transactions on Computers, Vol. C-28, pp. 178\u2013184, 1979.","journal-title":"IEEE Transactions on Computers"},{"key":"267091_CR10","first-page":"23","volume-title":"Proc. of the Int. Congr. of Mathematicians","author":"A. Church","year":"1962","unstructured":"A. Church, \u201cLogic, arithmetic and automata,\u201d in Proc. of the Int. Congr. of Mathematicians, Stockholm, 1962, Almquist and Wiksells, 1963, pp. 23\u201335."},{"key":"267091_CR11","doi-asserted-by":"crossref","unstructured":"A.G. Dragalin, Mathematical Intuitionism. Introduction to Proof Theory, American Mathematical Society,1988.","DOI":"10.1090\/mmono\/067"},{"issue":"3","key":"267091_CR12","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"R. Dyckhoff, \u201cContraction-free sequent calculi for intuitionistic logic,\u201d The Journal of Symbolic Logic, Vol.57, No. 3, pp. 795\u2013807, September 1992.","journal-title":"The Journal of Symbolic Logic"},{"key":"267091_CR13","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1147\/rd.92.0090","volume":"9","author":"E.B. Eichelberger","year":"1965","unstructured":"E.B. Eichelberger, \u201cHazard detection in combinational and sequential switching circuits,\u201d IBM J. Res. Div., Vol. 9, pp. 90\u201399, 1965.","journal-title":"IBM J. Res. Div."},{"key":"267091_CR14","doi-asserted-by":"crossref","unstructured":"H. Eveking and Ch. Mai, \u201cFormal verification of timing conditions,\u201d in European Design Automation Conference,1990, pp. 512\u2013517.","DOI":"10.1109\/EDAC.1990.136701"},{"issue":"1","key":"267091_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"M. Fairtlough and M. Mendler, \u201cPropositional lax logic,\u201d Information and Computation, Vol. 137, No. 1, pp.1\u201333, August 1997.","journal-title":"Information and Computation"},{"key":"267091_CR16","doi-asserted-by":"crossref","unstructured":"M. Fourman, \u201c Proof and design,\u201d in M. Broy (Ed.), Deductive Program Design, Springer, 1996, pp. 397\u2013439.","DOI":"10.1007\/978-3-642-61455-2_18"},{"key":"267091_CR17","unstructured":"T. Franz\u00e9n, \u201cAlgorithmic aspects of intuitionistic propositional logic,\u201d Research Report SICS R87010, Swedish Institute of Computer Science, 1987."},{"key":"267091_CR18","unstructured":"J. Fr\u00f6l and Th. Kropf, \u201cA new model to uniformly represent function and timing of MOS circuits and its application to VHDL simulation,\u201d in European Design Automation Conference, 1994."},{"key":"267091_CR19","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen, \u201cUntersuchungen \u00fcber das Logische Schlie\u03b2en,\u201d Math. Z., Vol. 39, pp. 176\u2013210, 405-431,1934-1935.","journal-title":"Math. Z."},{"key":"267091_CR20","unstructured":"J.Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, 1989."},{"key":"267091_CR21","first-page":"65","volume":"69","author":"K. G\u00f6del","year":"1932","unstructured":"K. G\u00f6del, \u201cZum Intuitionistischen Aussagenkalk\u00fcl,\u201d Akademie der Wissenschaften in Wien, Mathematisch-Naturwissenschaftliche Klasse. Anzeiger., Vol. 69, pp. 65\u201366, 1932.","journal-title":"Akademie der Wissenschaften in Wien, Mathematisch-Naturwissenschaftliche Klasse. Anzeiger"},{"key":"267091_CR22","unstructured":"M. Gordon, \u201cWhy higher-order logic is a good formalism for specifying and verifying hardware,\u201d in P.A. Subrahmanyam and G. Milne (Eds.), Formal Aspects of VLSI Design, North Holland, 1986, pp. 153\u2013178."},{"key":"267091_CR23","first-page":"409","volume-title":"Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design","author":"M.J.C. Gordon","year":"1990","unstructured":"M.J.C. Gordon, P. Loewenstein, and M. Shahaf, \u201cFormal verification of a cell library: A case study in technology transfer,\u201d in L.J.M. Claesen (Ed.), Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1990, North-Holland, Vol. 2, pp. 409\u2013417."},{"key":"267091_CR24","unstructured":"C.T. Gray, W. Liu, and R.K. Cavin III, \u201cExact timing analysis considering data dependent delays,\u201d in Internatinal Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Malente, September1993. ACM\/GMD."},{"key":"267091_CR25","unstructured":"D.J. Gurr, \u201cSemantic frameworks for complexity,\u201d PhD Thesis, Edinburgh University, Department of Computer Science, January 1991."},{"key":"267091_CR26","unstructured":"S. Hayashi and H. Nakano, PX, A Computational Logic, MIT Press, 1989."},{"issue":"2","key":"267091_CR27","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/TC.1986.1676728","volume":"C-35","author":"J.P. Hayes","year":"1986","unstructured":"J.P. Hayes, \u201cUncertainty, energy, and multiple-valued logics,\u201d IEEE Transactions on Computers, Vol. C-35, No. 2, pp. 107\u2013114, February 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"267091_CR28","unstructured":"J. Herbert, \u201cFormal verification of basic memory devices,\u201d Technical Report 124, University of Cambridge, Computer Laboratory, February 1988."},{"key":"267091_CR29","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare, \u201cA theory for the derivation of C-mos circuit designs,\u201d in W.H.J. Feijen, A.J.M. van Fasteren, D. Fries, and J. Misra (Eds.), Beauty is our Business, Springer, 1990.","DOI":"10.1007\/978-1-4612-4476-9_23"},{"key":"267091_CR30","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"S.C. Kleene, Introduction to Metamathematics, North Holland, Amsterdam, 1952, Ch. XII, Par. 64."},{"key":"267091_CR31","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/BF01186549","volume":"35","author":"A. Kolmogoroff","year":"1932","unstructured":"A. Kolmogoroff, \u201cZur Deutung der intuitionistischen Logik,\u201d Mathematische Zeitschrift, Vol. 35, pp. 58\u201365,1932.","journal-title":"Mathematische Zeitschrift"},{"key":"267091_CR32","doi-asserted-by":"crossref","unstructured":"K.C. Lam and R.K. Brayton, Timed Boolean Functions. A Unified Formalism for Exact Timing Analysis, Kluwer, 1994.","DOI":"10.1007\/978-1-4615-2688-9"},{"key":"267091_CR33","doi-asserted-by":"crossref","unstructured":"S. Malik, \u201cAnalysis of cyclic combinational circuits,\u201d in International Conference on Computer-Aided Design, IEEE, 1993, pp. 618\u2013625.","DOI":"10.1109\/ICCAD.1993.580150"},{"key":"267091_CR34","unstructured":"T. Margaria and M. Mendler, \u201cModel-based automatic synthesis and analysis in second-order monadic logic,\u201d in Proceedings First ACM SIGPLAN Workshop on Automated Analysis of Software, Paris, France, January1997, pp. 99\u2013112."},{"issue":"2","key":"267091_CR35","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/TC.1981.6312173","volume":"30","author":"L.R. Marino","year":"1981","unstructured":"L.R. Marino, \u201cGeneral theory of metastable operation,\u201d IEEE Transactions on Computers, Vol. 30, No. 2, pp.107\u2013115, February 1981.","journal-title":"IEEE Transactions on Computers"},{"key":"267091_CR36","doi-asserted-by":"crossref","unstructured":"P.C. McGeer and R.K. Brayton, Integrating Functional and Temporal Domains in Logic Design, Kluwer,1991.","DOI":"10.1007\/978-1-4615-3960-5"},{"issue":"4","key":"267091_CR37","first-page":"857","volume":"7","author":"J. Medvedev","year":"1966","unstructured":"Ju.T. Medvedev, \u201cInterpretation of logical formulas by means of finite problems,\u201d Soviet Math. Dokl., Vol. 7, No. 4, pp. 857\u2013860, 1966.","journal-title":"Soviet Math. Dokl."},{"key":"267091_CR38","first-page":"132","volume-title":"Workshop on Logic, Language, Information, and Computation","author":"M. Mendler","year":"1998","unstructured":"M. Mendler, \u201cCharacterising timing analysis in intuitionistic modal logic,\u201d in R.J.G.B. de Queiroz and M. Finger (Eds.), Workshop on Logic, Language, Information, and Computation, Department of Computer Science, IME\/USP University of S\u00e3o Paulo, Brazil, 1998, pp. 132\u2013140."},{"key":"267091_CR39","doi-asserted-by":"crossref","unstructured":"M. Mendler and M. Fairtlough, \u201cTernary simulation: A refinement of binary functions or an abstraction of real-time behaviour?\u201d in M. Sheeran and S. Singh (Eds.), Proceedings of the 3rd Workshop on Designing Correct Circuits (DCC96), Springer, October 1996. Springer Electronic Workshops in Computing.","DOI":"10.14236\/ewic\/DCC1996.8"},{"issue":"3","key":"267091_CR40","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF01384075","volume":"3","author":"M. Mendler","year":"1993","unstructured":"M. Mendler and T. Stroup, \u201cNewtonian arbiters cannot be proven correct,\u201d Formal Methods in System Design, Vol. 3, No. 3, pp. 233\u2013257, November\/December 1993.","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"267091_CR41","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1305\/ndjfl\/1093635238","volume":"30","author":"P. Miglioli","year":"1989","unstructured":"P. Miglioli, U. Moscato, M. Ornaghi, S. Quazza, and G. Usberti, \u201cSome results on intermediate constructive logics,\u201d Notre Dame Journal of Formal Logic, Vol. 30, No. 4, pp. 543\u2013562, 1989.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"267091_CR42","doi-asserted-by":"crossref","unstructured":"I. Mitchell and M.R. Greenstreet, \u201cProving newtonian arbiters correct, almost surely,\u201d in M. Sheeran and S. Singh (Eds.), Designing Correct Circuits, Springer Electronic Workshops in Computing, 1996.","DOI":"10.14236\/ewic\/DCC1996.10"},{"key":"267091_CR43","unstructured":"E. Moggi, \u201cThe partial lambda calculus,\u201d PhDThesis, Edinburgh University, Department of Computer Science, August 1988."},{"key":"267091_CR44","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"E. Moggi, \u201cNotions of computation and monads,\u201d Information and Computation, Vol. 93, pp. 55\u201392, 1991.","journal-title":"Information and Computation"},{"issue":"2","key":"267091_CR45","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","unstructured":"B. Moszkowski, \u201cA temporal logic for multilevel reasoning about hardware,\u201d IEEE Computer, Vol. 18, No.2, pp. 10\u201319, 1985.","journal-title":"IEEE Computer"},{"key":"267091_CR46","doi-asserted-by":"crossref","unstructured":"M. Parigot, \u201cProgramming with proofs: A second-order type theory,\u201d in H. Ganzinger (Ed.), European Symposium on Programming. LNCS, Vol. 300, Springer, 1988, pp. 145\u2013159.","DOI":"10.1007\/3-540-19027-9_10"},{"key":"267091_CR47","doi-asserted-by":"crossref","unstructured":"K. Sch\u00fctte, Systeme Modaler und Intuitionistischer Logik, Vol. 42, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer, 1968.","DOI":"10.1007\/978-3-642-88664-5"},{"key":"267091_CR48","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1973","unstructured":"R. Statman, \u201cIntuitionistic propositional logic is polynomial space complete,\u201d Theoretical Computer Science,Vol. 9, pp. 67\u201372, 1973.","journal-title":"Theoretical Computer Science"},{"key":"267091_CR49","doi-asserted-by":"crossref","unstructured":"P.A. Subrahmanyam, \u201cTowards a framework for dealing with system timing in very high level silicon compilers,\u201d in G. Birtwistle and P. Subrahmanyam (Eds.), VLSI Specification, Verification, and Synthesis, Kluwer,1988, pp. 159\u2013215. Workshop on Hardware Verification.","DOI":"10.1007\/978-1-4613-2007-4_5"},{"key":"267091_CR50","volume-title":"BinProlog 4.0 User Guide","author":"P. Tharau","year":"1995","unstructured":"P. Tharau, BinProlog 4.0 User Guide, Department d'Informatique, Universit\u00e9 de Moncton, Canada, September1995."},{"key":"267091_CR51","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra, \u201cRealizability,\u201d in S.R. Buss (Ed.), Handbook of Proof Theory, Elsevier, 1998, Ch. VI, pp.407\u2013474.","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"267091_CR52","doi-asserted-by":"crossref","unstructured":"D. van Dalen, \u201cIntuitionistic logic,\u201d in D. Gabbay and F. Guenthner (Ed.), Handbook of Philosophical Logic, Vol. III, Reidel, 1986, Ch. 4, pp. 225\u2013339.","DOI":"10.1007\/978-94-009-5203-4_4"},{"issue":"3","key":"267091_CR53","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1109\/TC.1982.1675978","volume":"C-31","author":"G. von Bochmann","year":"1982","unstructured":"G. von Bochmann, \u201cHardware specification with temporal logic: An example,\u201d IEEE Transactions on Computers, Vol. C-31, No. 3, pp. 223\u2013231, March 1982.","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"267091_CR54","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1109\/43.45866","volume":"9","author":"D. Weise","year":"1990","unstructured":"D. Weise, \u201cMultilevel verification of MOS circuits,\u201d IEEE Transactions on Computer-Aided Design, Vol. 9, No. 4, pp. 341\u2013351, April 1990.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"267091_CR55","doi-asserted-by":"crossref","unstructured":"G. Winskel, \u201cA compositional model of MOS circuits,\u201d in G.M. Birtwistle and P.A. Subrahmanyam (Eds.), VLSI Specification, Verification and Synthesis, Kluwer, 1987.","DOI":"10.1007\/978-1-4613-2007-4_11"},{"key":"267091_CR56","doi-asserted-by":"crossref","unstructured":"M. Yoeli and J.A. Brzozowski, \u201cTernary simulation of binary gate networks,\u201d in J.M. Dunn and G. Epstein (Eds.), Modern Uses of Multiple-Valued Logic, D. Reidel, 1977, pp. 41\u201350.","DOI":"10.1007\/978-94-010-1161-7_3"},{"key":"267091_CR57","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/321203.321214","volume":"11","author":"M. Yoeli","year":"1964","unstructured":"M. Yoeli and S. Rinon, \u201cApplication of ternary algebra to the study of static hazards,\u201d Journal of the ACM, Vol. 11, pp. 84\u201397, 1964.","journal-title":"Journal of the ACM"},{"issue":"1","key":"267091_CR58","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF00464355","volume":"1","author":"C. Zhou","year":"1992","unstructured":"Chaochen Zhou and C.A.R. Hoare, \u201cA model for synchronous switching circuits and its theory of correctness,\u201d Formal Methods in System Design, Vol. 1, No. 1, pp. 7\u201328, July 1992.","journal-title":"Formal Methods in System Design"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008780817617.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008780817617\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008780817617.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:18:00Z","timestamp":1754367480000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008780817617"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,8]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,8]]}},"alternative-id":["267091"],"URL":"https:\/\/doi.org\/10.1023\/a:1008780817617","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,8]]}}}