Publikationen

• Mendler, Michael ; V. De Paiva:
  Constructive CK for Contexts .
  In: Serafini, L. ; Bouquet, P. (Hrsg.) : Vol. 136 of CEUR Workshop Proceedings
  (CRR-2005,, Paris,, July 2005).
  2005.

• Aguado, Joaquin ; Mendler, Michael:
  Constructive Game Semantics for Instantaneous Reactions .
  In: D. R. Ghica ; G. McCusker (Hrsg.) : Proceedings of GaLoP 2005
  (Games for Logics and Programming Languages,, Edinburgh,, April 2005).
  2005, S. 16-31.

• Aguado, Joaquin ; Mendler, Michael:
  Constructive Game Semantics for Instantaneous Reactions .
  Bamberg : Universität Bamberg. 2005
  (63). - Interner Bericht. 48 Seiten

• G. Lüttgen ; N. Martinez Madrid ; Mendler, Michael (Hrsg.):
  Proceedings Workshop Semantic Foundations of Engineering Design Languages .
  (SFEDL 2004, January 2005)
  Bd. 115. . : Elsevier, 2005

• Aguado, Joaquin ; Mendler, Michael:
  Towards Unit Testing for Communicating Stream X-machines Systems .
  In: Hierons, R. ; McMinn, P. (Hrsg.) : Proceedings of UK Software Testing Research
  (UKTest 2005,, Sheffield,, September 5-6).
  2005, S. 39-66.

• G. Lüttgen ; Mendler, Michael:
  When 1 Clock is Not Enough .
  In: Aceto, L. ; Gordon, A. D. (Hrsg.) : Algebraic Process Calculi, PA '05
  (The First Twenty Five Years and Beyond,, Bertinoro,, 2005).
  2005, S. 155-158. (BRICS Notes Series, Nr. NS-05-03)

• De Paiva, V. ; Gore, R. ; Mendler, Michael (Hrsg.):
  Modalities in Constructive Modal Logics and Type Theories .
  Oxford : Oxford University Press, 2004
  (Special Issue of Journal of Logic and Computation Bd. to appear)

• Broy, M. ; Lüttgen, G. ; Mendler, Michael (Hrsg.):
  Special Issue: Semantic Foundations of Engineering Design Languages .
  London : Springer, 2004
  (Journal of Formal Aspects of Computing Bd. to appear)

• Norton, B. ; Luettgen, G. ; Mendler, Michael:
  A compositional semantic theory for synchronous component-based design .
  In: Amadio, R. ; Lugiez, D. (Hrsg.) : Int`l Conference on Concurrency Theory
  (Concur`03, Marseille, Sept. 2003).
  Berlin u.a. : Springer, 2003, S. 461-476. (LNCS Bd. 2761)

• Aguado, Joaquin ; Luettgen, G. ; Mendler, Michael:
  A-maze-ing Esterel .
  In: Maraninchi, F. ; Girault, A. ; Rutten, E. (Hrsg.) : Synchronous Languages, Applications and Programming
  (SLAP`03, Porto, Portugal, July 2003).
  2003, S. 15 Seiten. (Electronic Notes in Theoretical Computer Science Bd. to appear)

• Fairtlough, M. ; Mendler, Michael:
  Intensional completeness in an extension of Goedel-Dummett logic .
  In: Studia Logica 73 (2003), S. 51-80

• Broy, M. ; Lüttgen, G. ; Mendler, Michael (Hrsg.):
  Where theory and practice meet .
  London : Springer, 2003
  (special Issue of Formal Aspects of Computing Bd. 15, Nr. 4).
  - 125 Seiten.

• Luettgen, G. ; Mendler, Michael:
  Axiomatizing an algebra of step reactions for synchronous languages .
  In: Brim, L. ; Jancar, P. ; Ketinsky, M. ; Kucera, A. (Hrsg.) : Int`l Conference on Concurrency Theory
  (CONCUR 02, Brno, August 2002).
  Berlin u.a. : Springer, 2002, S. 386-401. (LNCS Bd. 2421)

• Gore, R. ; Mendler, Michael ; De Paiva, V. (Hrsg.):
  Intuitionistic Modal Logic and Applications .
  (IMLA'02 Copenhagen, DK July 2002)
  2002.
  - 100 Seiten.

• Fairtlough, M. ; Mendler, Michael:
  On the logical content of computational type theory: A solution to Curry`s problem .
  In: Callaghan, P. ; Luo, Z. ; McKinna, J. ; Pollack, R. (Hrsg.) : Types for Proofs and Programs.
  Berlin u.a. : Springer, 2002, (LNCS Bd. 2277), S. 63-78.

• Lüttgen, G. ; Mendler, Michael ; Maraninchi, F. (Hrsg.):
  Proc. Semantic Foundations of Engineering Design Languages (SFEDL'02) .
  (SFEDL'02 Grenoble April 2002)
  2002.
  - 137 Seiten.

• Luettgen, G. ; Mendler, Michael:
  The intuitionism behind statecharts steps .
  In: ACM Transactions on Computational Logic 3 (2002), Nr. 1, S. 1-41

• Luettgen, G. ; Mendler, Michael:
  Towards a Model Theory for Esterel .
  In: Maraninchi, F. ; Girault, A. ; Rutten, E. (Hrsg.) : Synchronous Languages and Applications
  (SLAP`02, Grenoble, April 2002). Bd. 65.
  Tulane : Elsevier Science Publ., 2002, S. 15 Seiten. (Electronic Notes in Theoretical Computer Science)

• Fairtlough, M. ; Mendler, Michael ; Cheng, X.:
  Abstraction and refinement in higher-order logic .
  In: Boulton, R. J. ; Jackson, P. B. (Hrsg.) : International Conference on Theorem Proving in Higher-order Logic
  (TPHOLs`2001, Edinburgh, September 2001).
  2001, S. 201-216. (LNCS Bd. 2152)

• Alechina, N. ; Mendler, Michael ; de Paiva, V. ; Ritter, E.:
  Categorical and Kripke semantics for constructive S4 modal logic .
  In: Fribourg, L. (Hrsg.) : Computer Science Logic
  (CSL`01, Paris, September 2001).
  2001, S. 292-307. (LNCS Bd. 2142)

• Fairtlough, M. ; Mendler, Michael ; Moggi, E. (Hrsg.):
  Modalities in Type Theory .
  Cambridge : Cambridge University Press, 2001
  (Special Issue of Mathematical Structures in Computer Science Bd. 11, Nr. 4).
  - 90 Seiten.

• Cheng, X. ; Fairtlough, M. ; Mendler, Michael:
  Proofs as constraints for abstraction and refinement. .
  In: Egly, U. ; Fiedler, A. ; Horacek, H. ; Schmitt, S. (Hrsg.) : Workshop on Proof Transformations, Proof Presentations and Complexities of Proof
  (PTP '01, Siena, Universitá degli Studi di Siena, Dipartimento di Ingegneria dell'Informatione, June 2001).
  2001, S. 1-11.

• Luettgen, G ; Mendler, Michael:
  Statecharts: From visual syntax to model-theoretic semantics .
  In: Bauknecht, K. ; Brauer, W. ; Mueck, Th. (Hrsg.) : Wirtschaft und Wissenschaft in der Network Economy-Visionen und Wirklichkeit
  (Workshop on Integrating Diagrammatic and Formal Specification Techniques, Vienna, September 2001). Bd. 1.
  Wien : Austrian Computer Society, 2001, S. 615-621.

• Mendler, Michael:
  Characterising combinational timing analyses in intuitionistic modal logic .
  In: The Logic Journal of the IGPL 8 (2000), Nr. 6, S. 821-853

• Luettgen, G. ; Mendler, Michael:
  Fully-abstract statecharts semantics via intuitionistic Kripke models .
  In: Montanari, U. ; Rolim, J. ; Welzl, E. (Hrsg.) : 27th Int'l Colloquium on Automata, Languages and Programming
  (ICALP 2000).
  Berlin u.a. : Springer, 2000, S. 163-174. (LNCS Bd. 1853)

• Luettgen, G. ; Mendler, Michael:
  The intuitionism behind statecharts steps .
  Hampton, V.A., USA : NASA Langley Research Center. 2000
  (NASA, Institute for Computer Applications in Science and Engineering ICASE, Report CR-2000-210302). - Forschungsbericht. 40 Seiten

• Mendler, Michael:
  Timing analysis of combinational circuits in intuitionistic propositional logic .
  In: Formal Methods in System Design 17 (2000), Nr. 1, S. 5-37

• Lüttgen, G. ; Mendler, Michael:
  What is in a Step: A fully abstract semantics for Statecharts macro steps via intuitionistic Kripke models .
  Sheffield : University of Sheffield. 2000
  (CS-00-04). - Interner Bericht. 48 Seiten

• Lock, Th. ; Mendler, Michael ; Mutz, M.:
  Äquivalenz von annotierten Kontrollflußgraphen zur Darstellung von HLS-Ein- und -Ausgaben bei Verwendung pfadbasierter Einplanungsverfahren .
  In: Mutz, M. ; Lange, N. (Hrsg.) : GI/ITG/GMM Workshop: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen.
  Braunschweig : Shaker, 1999, S. 51-60.

• Mendler, Michael:
  Characterising timing analyses in intuitionistic modal logic .
  In: DeQueiroz, R., J., G., B. ; Finger, M. (Hrsg.) : Workshop on Logic, Language, Information, and Computation.
  Department of Computer Science : IME/USP University of Sao Paulo, Brazil, 1998, S. 132-140.

• Lock, Th. ; Mendler, Michael ; Mutz, M.:
  Combined formal post- and presynthesis verification in high level synthesis .
  In: Gopalakrishnan, G. ; Windley, Ph. (Hrsg.) : International Conference on Formal Methods in Computer-Aided Design (FMCAD '98).
  Berlin u.a. : Springer, 1998, (LNCS Bd. 1522), S. 222-236.

• Lock, Th. ; Mendler, Michael:
  Formale Modellierung von kontrollflußdominierten High-Level-Synthese-Eingabebeschreibungen zur Verifikation von Ergebnissen kontrollflußgesteuerter Einplanungsverfahren .
  In: Rammig, F., J. ; Müller, W. (Hrsg.) : Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen.
  Paderborn : HNI Verlagschriftenreihe, 1998, S. 75-84.

• Margaria, T. ; Mendler, Michael ; Gsottberger, C.:
  Modelling and verification of unbounded length systolic arrays in monadic second-order logic .
  In: University of Aalborg (Veranst.):
  Int'l. Workshop on Infinite State Systems
  (Infinity '98, Aalborg, DK, Juli 1998).
  München : TU München, 1998, S. 99-112.

• Sicheneder, A. ; Bender, A. ; Fuchs, E. ; Mendler, Michael ; Sick, B.:
  Tool-supported software design and program execution for signal processing applications using modular software components .
  In: Margaria, T. ; Steffen, B. (Hrsg.) : Proceedings International Workshop on Software Tools for Technology Transfer
  (STTT'98, University of Aalborg, Denmark, June 1998).
  1998, S. 61-70.

• Kelb, P. ; Margaria, T. ; Mendler, Michael ; Gsottberger, C.:
  A sound and efficient tool for M2L(Str.) .
  In: Grumberg, O. (Hrsg.) : Computer-Aided Verification (CAV '97).
  Berlin u.a. : Springer, 1997, (Lecture Notes in Computer Science Bd. 1254), S. 448-451.

• Cleaveland, R. ; Lüttgen, G. ; Mendler, Michael:
  An algebraic theory of multiple clocks .
  In: Mazurkiewicz, A. ; Winkowski, J. (Hrsg.) : Proceedings of the International Conference on Concurrency Theory (CONCUR '97).
  Berlin u.a. : Springer, 1997, S. 166-180. (LNCS Bd. 1243)

• Fairtlough, M. ; Mendler, Michael ; Walton, M.:
  First-order Lax Logic as a Framework for Constraint Logic Programming .
  Passau : Universität Passau. 1997
  (MIP-9714). - Forschungsbericht. 51 Seiten

• Margaria, T. ; Mendler, Michael:
  Model-based automatic synthesis and analysis in second-order monadic logic .
  In: ACM SIG-PLAN (Veranst.):
  Proceedings Workshop on Automated Analysis of Software
  (AAS'97, Paris, January 1997).
  Paris : ACM, 1997, S. 99-112.

• Kelb, P. ; Margaria, T. ; Mendler, Michael ; Gsottberger, C.:
  MOSEL: A flexible toolset for monadic second-order logic .
  In: Brinksma, E. (Hrsg.) : Proceedings Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97).
  Berlin u.a. : Springer, 1997, (LNCS Bd. 1217), S. 183-202.

• Fairtlough, M. ; Mendler, Michael:
  Propositional Lax Logic .
  In: Information and Computation Vol.137 (1997), Nr. 1, S. 1-33

• Margaria, T. ; Mendler, Michael:
  Automatic treatment of sequential circuits in second-order monadic logic .
  In: Straube, B. (Hrsg.) : GI/ITG/GME Workshop Methoden des Entwurfs und der Verifikation Digitaler Systeme.
  Aachen : Shaker, 1996, S. 21-30.

• Mendler, Michael ; Fairtlough, M.:
  Ternary simulation: A refinement of binary functions or abstraction of real-time behaviour?
  In: Sheeran, M. ; Singh, S. (Hrsg.) : Proceedings of the 3rd Workshop on Designing Correct Circuits
  (DCC`96).
  Berlin u.a. : Springer, 1996, S. 17 Seiten. (Springer Electronic Workshops in Computing)

• Mendler, Michael:
  Timing refinement of intuitionistic proofs .
  In: Straube, B. (Hrsg.) : GI/ITG/GME Workshop Methoden des Entwurfs und der Verifikation Digitaler Systeme.
  Aachen : Shaker, 1996, S. 121-130.

• Mendler, Michael:
  Timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits .
  In: Miglioli, P. ; Moscato, U. ; Mundici, D. ; Ornaghi, M. (Hrsg.) : Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods.
  Berlin u.a. : Springer, 1996, (LNAI Bd. 1071), S. 261-277.

• Wang, L., G. ; Mendler, Michael:
  Abstraction of hardware construction .
  In: Dowek, G. ; Heering, J. ; Möller, B. ; Meinke, K. (Hrsg.) : Higher-Order Algebra, Logic, and Term Rewriting. HOA'95.
  Bd. LNCS1074. Berlin u.a. : Springer, 1995, S. 264-287.

• Fairtlough, M. ; Mendler, Michael:
  An intuitionistic modal logic with applications to the formal verification of hardware .
  In: Pacholski, L. ; Tiuryn, J. (Hrsg.) : Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic.
  Berlin u. a. : Springer, 1995, S. 354-368. (LNCS Bd. 933)

• Mendler, Michael:
  Can we specify finite-state systems in a fragment of propositional logic?
  In: Straube, B. (Hrsg.) : Use of Process Algebras in Design
  (3rd Euroform Workshop, Februar 1995).
  Dresden : Fraunhofer Institut, 1995, S. 23 Seiten.

• Andersen, H. R. ; Mendler, Michael:
  Describing a signal analyzer in the process algebra PMC - A case study .
  In: Mosses, P.D. ; Nielsen, M. ; Schwartzbach, M.I. (Hrsg.) : Theory and Practice of Software Development (TAPSOFT '95).
  Berlin u.a. : Springer, 1995, (LNCS Bd. 915), S. 620-635.

• Fuchs, M. ; Mendler, Michael:
  Functional semantics for delta-VHDL based on FOCUS .
  In: Kloos, C.D. ; Breuer, P.T. (Hrsg.) : Formal Semantics for VHDL, chapter 1.
  Boston u.a. : Kluwer, 1995, S. 9-42.

• Wang, L., G. ; Mendler, Michael:
  The formal design of a class of computers - its high stage: Abstract microprogramming .
  In: Eveking, H. ; Camurati, P. (Hrsg.) : Correct Hardware Design and Verification Methods (CHARME '95).
  Berlin u.a. : Springer, 1995, (LNCS Bd. 789), S. 84-102.

• Andersen, H.R. ; Mendler, Michael:
  An asynchronous process algebra with multiple clocks .
  In: Sannella, D. (Hrsg.) : European Symposium on Programming.
  Berlin u.a. : Springer, 1994, S. 58-73. (LNCS Bd. 788)

• Mendler, Michael:
  Dealing with Hardware Constraints - A modal logical approach .
  In: Kloos, C., D. (Hrsg.) : 1st Euroform Workshop
  (1st Euroform Workshop, Las Navas del Marques, Spain, January 1994).
  1994, S. 7 Seiten.

• Andersen, H., R. ; Mendler, Michael:
  A complete axiomatization of observation congruence in PMC .
  Lyngby : Technical University of Denmark. 1993
  (ID-TR:1993-126). - Interner Bericht. 25 Seiten

• Mendler, Michael:
  A modal logic for handling behavioural constraints in formal hardware verification .
  Edinburgh : Dept. of Computer Science, University of Edinburgh. 1993
  (ECS-LFCS-93-255, March). - Forschungsbericht. 236 Seiten

• Andersen, H. R. ; Mendler, Michael:
  A process algebra with multiple clocks .
  Lyngby : Technical University of Denmark. 1993
  (ID-TR:1993-122). - Interner Bericht. 40 Seiten

• Mendler, Michael ; Stroup, T.:
  Newtonian arbiters cannot be proven correct .
  In: Formal Methods in System Design 3 (1993), Nr. 3, S. 233-257

• Steffen, B. ; Jay, C., B. ; Mendler, Michael:
  Compositional characterization of observable program properties .
  In: Theoretical Informatics and Applications 26 (1992), Nr. 5, S. 403-424

• Reinhardt, T. ; Mendler, Michael ; Stroup, T.:
  Die formale Validierung einer "Bausteintafel" delay-insensitiver Grundelemente .
  In: M. Glesner (Hrsg.) : Rechnergestützter Entwurf und Architektur mikroelektronischer Systeme
  (ITG-Fachbericht).
  Berlin und Offenbach : VDE Verlag, 1992, S. 273-274.

• Mendler, Michael ; Reinhardt, T. ; Stroup, T.:
  Konsistenz, Vollständigkeit und Kohärenz einer Bausteintafel delay-insensitiver Grundelemente. Technical Report .
  Erlangen : Institut für Mathem. Maschinen und Datenverarbeitung. 1992
  (IMMD7-15/92). - Interner Bericht

• Mendler, Michael ; Stroup, T.:
  Newtonian arbiters cannot be proven correct .
  In: Staunstrup J. ; Sharp, R. (Hrsg.) : Workshop on Designing Correct Circuits.
  Amsterdam and New York : North Holland, 1992, S. 47-66.

• Mendler, Michael:
  Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification .
  In: Jones, G. ; Sheeran, M. (Hrsg.) : Workshop on Designing Correct Circuits.
  Berlin u.a. : Springer, 1991, S. 1-28.

• Stroup, T. ; Götz, N. ; Mendler, Michael:
  Stepwise refinement of layered protocols by formal program development .
  In: Brinksma, E. ; Scollo, G. ; Visser, Ch., A. (Hrsg.) : 9th IFIP WG 6.1 Int'l Symposium on Protocol Specification, Testing, and Verification.
  Enschede : University of Twente, 1989, S. 14 Seiten.