Index of /~nad/listings/definitional-interpreters

	Name	Last modified	Size	Description
	Parent Directory		-
	Accessibility.html	2025-05-12 09:11	94K
	Agda.Builtin.Bool.html	2025-05-12 09:11	3.1K
	Agda.Builtin.Char.html	2025-05-12 09:11	4.0K
	Agda.Builtin.Equalit..>	2025-05-12 09:11	2.6K
	Agda.Builtin.Float.html	2025-05-12 09:11	32K
	Agda.Builtin.Int.html	2025-05-12 09:11	3.4K
	Agda.Builtin.List.html	2025-05-12 09:11	4.7K
	Agda.Builtin.Maybe.html	2025-05-12 09:11	2.3K
	Agda.Builtin.Nat.html	2025-05-12 09:11	23K
	Agda.Builtin.Reflect..>	2025-05-12 09:11	164K
	Agda.Builtin.Sigma.html	2025-05-12 09:11	3.4K
	Agda.Builtin.Size.html	2025-05-12 09:11	4.2K
	Agda.Builtin.Strict...>	2025-05-12 09:11	4.8K
	Agda.Builtin.String...>	2025-05-12 09:11	10K
	Agda.Builtin.Unit.html	2025-05-12 09:11	1.7K
	Agda.Builtin.Word.html	2025-05-12 09:11	2.0K
	Agda.Primitive.html	2025-05-12 09:11	5.4K
	Agda.css	2025-05-12 09:11	1.8K
	Algebra.Bundles.Raw...>	2025-05-12 09:11	66K
	Algebra.Bundles.html	2025-05-12 09:11	282K
	Algebra.Consequences..>	2025-05-12 09:11	9.5K
	Algebra.Consequences..>	2025-05-12 09:11	48K
	Algebra.Consequences..>	2025-05-12 09:11	179K
	Algebra.Construct.Li..>	2025-05-12 09:11	84K
	Algebra.Construct.Na..>	2025-05-12 09:11	17K
	Algebra.Construct.Na..>	2025-05-12 09:11	7.5K
	Algebra.Construct.Na..>	2025-05-12 09:11	18K
	Algebra.Construct.Na..>	2025-05-12 09:11	13K
	Algebra.Construct.Na..>	2025-05-12 09:11	56K
	Algebra.Construct.Na..>	2025-05-12 09:11	109K
	Algebra.Core.html	2025-05-12 09:11	3.3K
	Algebra.Definitions...>	2025-05-12 09:11	19K
	Algebra.Definitions...>	2025-05-12 09:11	11K
	Algebra.Definitions...>	2025-05-12 09:11	21K
	Algebra.Definitions...>	2025-05-12 09:11	118K
	Algebra.Lattice.Bund..>	2025-05-12 09:11	7.4K
	Algebra.Lattice.Bund..>	2025-05-12 09:11	53K
	Algebra.Lattice.Cons..>	2025-05-12 09:11	4.8K
	Algebra.Lattice.Cons..>	2025-05-12 09:11	19K
	Algebra.Lattice.Cons..>	2025-05-12 09:11	6.5K
	Algebra.Lattice.Prop..>	2025-05-12 09:11	292K
	Algebra.Lattice.Prop..>	2025-05-12 09:11	6.2K
	Algebra.Lattice.Prop..>	2025-05-12 09:11	43K
	Algebra.Lattice.Prop..>	2025-05-12 09:11	11K
	Algebra.Lattice.Stru..>	2025-05-12 09:11	40K
	Algebra.Morphism.Def..>	2025-05-12 09:11	11K
	Algebra.Morphism.Str..>	2025-05-12 09:11	210K
	Algebra.Morphism.html	2025-05-12 09:11	47K
	Algebra.Properties.A..>	2025-05-12 09:11	13K
	Algebra.Properties.C..>	2025-05-12 09:11	112K
	Algebra.Properties.G..>	2025-05-12 09:11	70K
	Algebra.Properties.L..>	2025-05-12 09:11	21K
	Algebra.Properties.M..>	2025-05-12 09:11	32K
	Algebra.Properties.Q..>	2025-05-12 09:11	17K
	Algebra.Properties.R..>	2025-05-12 09:11	6.4K
	Algebra.Properties.R..>	2025-05-12 09:11	44K
	Algebra.Properties.S..>	2025-05-12 09:11	8.2K
	Algebra.Properties.S..>	2025-05-12 09:11	39K
	Algebra.Solver.Ring...>	2025-05-12 09:11	45K
	Algebra.Solver.Ring...>	2025-05-12 09:11	96K
	Algebra.Solver.Ring...>	2025-05-12 09:11	4.6K
	Algebra.Solver.Ring...>	2025-05-12 09:11	288K
	Algebra.Structures.B..>	2025-05-12 09:11	65K
	Algebra.Structures.html	2025-05-12 09:11	233K
	Algebra.html	2025-05-12 09:11	1.9K
	Axiom.Extensionality..>	2025-05-12 09:11	21K
	Axiom.UniquenessOfId..>	2025-05-12 09:11	21K
	Bijection.html	2025-05-12 09:11	226K
	Bool.html	2025-05-12 09:11	74K
	Bounded-space.html	2025-05-12 09:11	91K
	Colist.html	2025-05-12 09:11	375K
	Conat.html	2025-05-12 09:11	432K
	Data.Bool.Base.html	2025-05-12 09:11	13K
	Data.Bool.ListAction..>	2025-05-12 09:11	7.3K
	Data.Bool.Properties..>	2025-05-12 09:11	207K
	Data.Empty.Polymorph..>	2025-05-12 09:11	4.5K
	Data.Empty.html	2025-05-12 09:11	5.0K
	Data.Fin.Base.html	2025-05-12 09:11	114K
	Data.Fin.Patterns.html	2025-05-12 09:11	4.7K
	Data.Fin.Properties...>	2025-05-12 09:11	547K
	Data.Irrelevant.html	2025-05-12 09:11	12K
	Data.List.Base.html	2025-05-12 09:11	223K
	Data.List.Effectful...>	2025-05-12 09:11	147K
	Data.List.Extrema.Co..>	2025-05-12 09:11	62K
	Data.List.Extrema.html	2025-05-12 09:11	132K
	Data.List.Membership..>	2025-05-12 09:11	44K
	Data.List.Membership..>	2025-05-12 09:11	239K
	Data.List.Membership..>	2025-05-12 09:11	9.3K
	Data.List.Membership..>	2025-05-12 09:11	261K
	Data.List.Membership..>	2025-05-12 09:11	20K
	Data.List.Properties..>	2025-05-12 09:11	867K
	Data.List.Relation.B..>	2025-05-12 09:11	6.9K
	Data.List.Relation.B..>	2025-05-12 09:11	51K
	Data.List.Relation.B..>	2025-05-12 09:11	31K
	Data.List.Relation.B..>	2025-05-12 09:11	37K
	Data.List.Relation.B..>	2025-05-12 09:11	132K
	Data.List.Relation.B..>	2025-05-12 09:11	2.8K
	Data.List.Relation.B..>	2025-05-12 09:11	11K
	Data.List.Relation.U..>	2025-05-12 09:11	49K
	Data.List.Relation.U..>	2025-05-12 09:11	388K
	Data.List.Relation.U..>	2025-05-12 09:11	112K
	Data.List.Relation.U..>	2025-05-12 09:11	6.3K
	Data.List.Relation.U..>	2025-05-12 09:11	36K
	Data.List.Relation.U..>	2025-05-12 09:11	459K
	Data.List.Relation.U..>	2025-05-12 09:11	38K
	Data.List.Relation.U..>	2025-05-12 09:11	3.8K
	Data.Maybe.Base.html	2025-05-12 09:11	37K
	Data.Maybe.Relation...>	2025-05-12 09:11	56K
	Data.Maybe.Relation...>	2025-05-12 09:11	33K
	Data.Nat.Base.html	2025-05-12 09:11	103K
	Data.Nat.DivMod.Core..>	2025-05-12 09:11	224K
	Data.Nat.DivMod.html	2025-05-12 09:11	356K
	Data.Nat.Divisibilit..>	2025-05-12 09:11	16K
	Data.Nat.Divisibilit..>	2025-05-12 09:11	170K
	Data.Nat.Generalised..>	2025-05-12 09:11	68K
	Data.Nat.Induction.html	2025-05-12 09:11	25K
	Data.Nat.Properties...>	2025-05-12 09:11	938K
	Data.Nat.Solver.html	2025-05-12 09:11	2.4K
	Data.Parity.Base.html	2025-05-12 09:11	19K
	Data.Product.Algebra..>	2025-05-12 09:11	55K
	Data.Product.Base.html	2025-05-12 09:11	87K
	Data.Product.Functio..>	2025-05-12 09:11	163K
	Data.Product.Functio..>	2025-05-12 09:11	49K
	Data.Product.Functio..>	2025-05-12 09:11	59K
	Data.Product.Propert..>	2025-05-12 09:11	57K
	Data.Product.Relatio..>	2025-05-12 09:11	97K
	Data.Product.Relatio..>	2025-05-12 09:11	5.4K
	Data.Sign.Base.html	2025-05-12 09:11	8.9K
	Data.Sum.Algebra.html	2025-05-12 09:11	33K
	Data.Sum.Base.html	2025-05-12 09:11	26K
	Data.Sum.Function.Pr..>	2025-05-12 09:11	46K
	Data.Sum.Function.Se..>	2025-05-12 09:11	73K
	Data.Sum.Properties...>	2025-05-12 09:11	60K
	Data.Sum.Relation.Bi..>	2025-05-12 09:11	106K
	Data.Sum.html	2025-05-12 09:11	12K
	Data.These.Base.html	2025-05-12 09:11	37K
	Data.Unit.Base.html	2025-05-12 09:11	1.9K
	Data.Unit.Polymorphi..>	2025-05-12 09:11	3.6K
	Data.Unit.Polymorphi..>	2025-05-12 09:11	27K
	Data.Unit.Polymorphi..>	2025-05-12 09:11	1.9K
	Data.Vec.Base.html	2025-05-12 09:11	150K
	Data.Vec.Bounded.Bas..>	2025-05-12 09:11	68K
	Data.Vec.Functional...>	2025-05-12 09:11	67K
	Data.Vec.N-ary.html	2025-05-12 09:11	92K
	Data.Vec.html	2025-05-12 09:11	12K
	Delay-monad.Always.html	2025-05-12 09:11	14K
	Delay-monad.Bisimila..>	2025-05-12 09:11	9.0K
	Delay-monad.Bisimila..>	2025-05-12 09:11	246K
	Delay-monad.Monad.html	2025-05-12 09:11	61K
	Delay-monad.Parallel..>	2025-05-12 09:11	137K
	Delay-monad.Quantita..>	2025-05-12 09:11	426K
	Delay-monad.Sequenti..>	2025-05-12 09:11	104K
	Delay-monad.Terminat..>	2025-05-12 09:11	42K
	Delay-monad.html	2025-05-12 09:11	16K
	Double-negation.html	2025-05-12 09:11	96K
	Effect.Applicative.html	2025-05-12 09:11	36K
	Effect.Choice.html	2025-05-12 09:11	4.4K
	Effect.Empty.html	2025-05-12 09:11	3.8K
	Effect.Functor.html	2025-05-12 09:11	13K
	Effect.Monad.html	2025-05-12 09:11	35K
	Embedding.html	2025-05-12 09:11	93K
	Equality.Decidable-U..>	2025-05-12 09:11	76K
	Equality.Decision-pr..>	2025-05-12 09:11	97K
	Equality.Instances-r..>	2025-05-12 09:11	120K
	Equality.Proposition..>	2025-05-12 09:11	19K
	Equality.html	2025-05-12 09:11	1.0M
	Equivalence-relation..>	2025-05-12 09:11	82K
	Equivalence.Contract..>	2025-05-12 09:11	128K
	Equivalence.Erased.B..>	2025-05-12 09:11	97K
	Equivalence.Erased.C..>	2025-05-12 09:11	71K
	Equivalence.Half-adj..>	2025-05-12 09:11	133K
	Equivalence.List.html	2025-05-12 09:11	355K
	Equivalence.Path-spl..>	2025-05-12 09:11	413K
	Equivalence.html	2025-05-12 09:11	502K
	Erased.Basics.html	2025-05-12 09:11	14K
	Erased.Box-cong-axio..>	2025-05-12 09:11	7.0K
	Erased.Level-1.html	2025-05-12 09:11	1.2M
	Excluded-middle.html	2025-05-12 09:11	6.6K
	Extensionality.html	2025-05-12 09:11	189K
	For-iterated-equalit..>	2025-05-12 09:11	337K
	Function-universe.html	2025-05-12 09:11	2.6M
	Function.Base.html	2025-05-12 09:11	76K
	Function.Bundles.html	2025-05-12 09:11	128K
	Function.Consequence..>	2025-05-12 09:11	12K
	Function.Consequence..>	2025-05-12 09:11	23K
	Function.Consequence..>	2025-05-12 09:11	35K
	Function.Construct.C..>	2025-05-12 09:11	119K
	Function.Construct.I..>	2025-05-12 09:11	46K
	Function.Construct.S..>	2025-05-12 09:11	72K
	Function.Core.html	2025-05-12 09:11	5.0K
	Function.Definitions..>	2025-05-12 09:11	21K
	Function.Dependent.B..>	2025-05-12 09:11	9.3K
	Function.Indexed.Rel..>	2025-05-12 09:11	8.2K
	Function.Metric.Bund..>	2025-05-12 09:11	37K
	Function.Metric.Core..>	2025-05-12 09:11	2.8K
	Function.Metric.Defi..>	2025-05-12 09:11	35K
	Function.Metric.Nat...>	2025-05-12 09:11	29K
	Function.Metric.Nat...>	2025-05-12 09:11	2.8K
	Function.Metric.Nat...>	2025-05-12 09:11	18K
	Function.Metric.Nat...>	2025-05-12 09:11	19K
	Function.Metric.Nat...>	2025-05-12 09:11	1.8K
	Function.Metric.Stru..>	2025-05-12 09:11	22K
	Function.Properties...>	2025-05-12 09:11	21K
	Function.Properties...>	2025-05-12 09:11	46K
	Function.Properties...>	2025-05-12 09:11	53K
	Function.Properties...>	2025-05-12 09:11	19K
	Function.Properties...>	2025-05-12 09:11	23K
	Function.Related.Pro..>	2025-05-12 09:11	120K
	Function.Related.Typ..>	2025-05-12 09:11	165K
	Function.Structures...>	2025-05-12 09:11	47K
	Groupoid.html	2025-05-12 09:11	189K
	H-level.Closure.html	2025-05-12 09:11	406K
	H-level.html	2025-05-12 09:11	53K
	Induction.WellFounde..>	2025-05-12 09:11	96K
	Induction.html	2025-05-12 09:11	14K
	Injection.html	2025-05-12 09:11	18K
	Integer.Basics.html	2025-05-12 09:11	40K
	Lambda.Compiler-corr..>	2025-05-12 09:11	257K
	Lambda.Compiler-corr..>	2025-05-12 09:11	241K
	Lambda.Compiler-corr..>	2025-05-12 09:11	173K
	Lambda.Compiler.html	2025-05-12 09:11	33K
	Lambda.Delay-crash-t..>	2025-05-12 09:11	100K
	Lambda.Delay-crash.html	2025-05-12 09:11	142K
	Lambda.Interpreter.S..>	2025-05-12 09:11	15K
	Lambda.Interpreter.S..>	2025-05-12 09:11	41K
	Lambda.Interpreter.S..>	2025-05-12 09:11	130K
	Lambda.Interpreter.S..>	2025-05-12 09:11	34K
	Lambda.Interpreter.S..>	2025-05-12 09:11	35K
	Lambda.Interpreter.html	2025-05-12 09:11	24K
	Lambda.Syntax.html	2025-05-12 09:11	43K
	Lambda.Type-soundnes..>	2025-05-12 09:11	52K
	Lambda.Virtual-machi..>	2025-05-12 09:11	12K
	Lambda.Virtual-machi..>	2025-05-12 09:11	36K
	Level.html	2025-05-12 09:11	5.6K
	List.html	2025-05-12 09:11	265K
	Logical-equivalence...>	2025-05-12 09:11	50K
	Maybe.html	2025-05-12 09:11	52K
	Modality.Basics.html	2025-05-12 09:11	2.1M
	Monad.Raw.html	2025-05-12 09:11	18K
	Monad.State.html	2025-05-12 09:11	37K
	Monad.html	2025-05-12 09:11	115K
	Nat.Solver.html	2025-05-12 09:11	59K
	Nat.html	2025-05-12 09:11	476K
	Omniscience.html	2025-05-12 09:11	55K
	Only-allocation.html	2025-05-12 09:11	6.9K
	Preimage.html	2025-05-12 09:11	59K
	Prelude.Size.html	2025-05-12 09:11	3.1K
	Prelude.html	2025-05-12 09:11	123K
	Pullback.html	2025-05-12 09:11	102K
	Relation.Binary.Bund..>	2025-05-12 09:11	12K
	Relation.Binary.Bund..>	2025-05-12 09:11	98K
	Relation.Binary.Cons..>	2025-05-12 09:11	101K
	Relation.Binary.Cons..>	2025-05-12 09:11	50K
	Relation.Binary.Cons..>	2025-05-12 09:11	77K
	Relation.Binary.Cons..>	2025-05-12 09:11	82K
	Relation.Binary.Cons..>	2025-05-12 09:11	80K
	Relation.Binary.Cons..>	2025-05-12 09:11	73K
	Relation.Binary.Core..>	2025-05-12 09:11	19K
	Relation.Binary.Defi..>	2025-05-12 09:11	98K
	Relation.Binary.Inde..>	2025-05-12 09:11	12K
	Relation.Binary.Inde..>	2025-05-12 09:11	17K
	Relation.Binary.Inde..>	2025-05-12 09:11	13K
	Relation.Binary.Inde..>	2025-05-12 09:11	11K
	Relation.Binary.Inde..>	2025-05-12 09:11	14K
	Relation.Binary.Inde..>	2025-05-12 09:11	2.1K
	Relation.Binary.Latt..>	2025-05-12 09:11	69K
	Relation.Binary.Latt..>	2025-05-12 09:11	13K
	Relation.Binary.Latt..>	2025-05-12 09:11	63K
	Relation.Binary.Latt..>	2025-05-12 09:11	1.7K
	Relation.Binary.Morp..>	2025-05-12 09:11	6.3K
	Relation.Binary.Morp..>	2025-05-12 09:11	38K
	Relation.Binary.Prop..>	2025-05-12 09:11	16K
	Relation.Binary.Prop..>	2025-05-12 09:11	34K
	Relation.Binary.Prop..>	2025-05-12 09:11	11K
	Relation.Binary.Prop..>	2025-05-12 09:11	24K
	Relation.Binary.Prop..>	2025-05-12 09:11	18K
	Relation.Binary.Prop..>	2025-05-12 09:11	7.0K
	Relation.Binary.Prop..>	2025-05-12 09:11	37K
	Relation.Binary.Prop..>	2025-05-12 09:11	110K
	Relation.Binary.Prop..>	2025-05-12 09:11	51K
	Relation.Binary.Reas..>	2025-05-12 09:11	32K
	Relation.Binary.Reas..>	2025-05-12 09:11	14K
	Relation.Binary.Reas..>	2025-05-12 09:11	54K
	Relation.Binary.Reas..>	2025-05-12 09:11	3.7K
	Relation.Binary.Reas..>	2025-05-12 09:11	5.4K
	Relation.Binary.Reas..>	2025-05-12 09:11	90K
	Relation.Binary.Refl..>	2025-05-12 09:11	37K
	Relation.Binary.Stru..>	2025-05-12 09:11	10K
	Relation.Binary.Stru..>	2025-05-12 09:11	68K
	Relation.Binary.html	2025-05-12 09:11	2.1K
	Relation.Nullary.Dec..>	2025-05-12 09:11	69K
	Relation.Nullary.Dec..>	2025-05-12 09:11	39K
	Relation.Nullary.Ind..>	2025-05-12 09:11	3.2K
	Relation.Nullary.Neg..>	2025-05-12 09:11	21K
	Relation.Nullary.Neg..>	2025-05-12 09:11	38K
	Relation.Nullary.Rec..>	2025-05-12 09:11	20K
	Relation.Nullary.Ref..>	2025-05-12 09:11	42K
	Relation.Nullary.html	2025-05-12 09:11	6.3K
	Relation.Unary.Predi..>	2025-05-12 09:11	44K
	Relation.Unary.Prope..>	2025-05-12 09:11	123K
	Relation.Unary.html	2025-05-12 09:11	93K
	Surjection.html	2025-05-12 09:11	88K
	TC-monad.html	2025-05-12 09:11	170K
	Tactic.By.Propositio..>	2025-05-12 09:11	121K
	Tactic.By.html	2025-05-12 09:11	145K
	Unbounded-space.html	2025-05-12 09:11	192K
	Univalence-axiom.html	2025-05-12 09:11	706K
	Upper-bounds.html	2025-05-12 09:11	298K
	Vec.Data.html	2025-05-12 09:11	39K
	Vec.Dependent.html	2025-05-12 09:11	47K

------------------------------------------------------------------------
-- Code related to the paper "Total Definitional Interpreters for Time
-- and Space Complexity"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Note that the code has evolved after the paper was written. For
-- code that is closer to the paper, see the version of the code that
-- is distributed with the paper.

module README where

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Responses to some challenges from Ancona, Dagnino and Zucca

-- The syntax of a toy programming language that only supports
-- allocation and deallocation of memory.

import Only-allocation

-- Definitional interpreters can model systems with bounded space.

import Bounded-space

-- Upper bounds of colists containing natural numbers.

import Upper-bounds

-- Definitional interpreters can model systems with unbounded space.

import Unbounded-space

------------------------------------------------------------------------
-- An example involving a simple λ-calculus

-- Some developments based on "Operational Semantics Using the
-- Partiality Monad" by Danielsson.
--
-- These developments to a large extent mirror developments in
-- "Coinductive big-step operational semantics" by Leroy and Grall.
--
-- The main differences compared to those two pieces of work are
-- perhaps the following ones:
--
-- * Sized types are used.
--
-- * The infinite set of uninterpreted constants has been replaced by
--   booleans, and definitions (named, unary, recursive functions)
--   are included.
--
-- * The virtual machine and the compiler include support for tail
--   calls.
--
-- * Stack space usage is analysed.

-- The syntax of, and a type system for, an untyped λ-calculus with
-- booleans and recursive unary function calls.

import Lambda.Syntax

-- A delay monad with the possibility of crashing.

import Lambda.Delay-crash

-- A definitional interpreter.

import Lambda.Interpreter

-- A type soundness result.

import Lambda.Type-soundness

-- A combination of the delay monad (with the possibility of crashing)
-- and a kind of writer monad yielding colists.

import Lambda.Delay-crash-trace

-- Virtual machine instructions, state etc.

import Lambda.Virtual-machine.Instructions

-- A virtual machine.

import Lambda.Virtual-machine

-- A compiler.

import Lambda.Compiler

-- Compiler correctness.

import Lambda.Compiler-correctness

-- A definitional interpreter that is instrumented with information
-- about the stack size of the compiled program.

import Lambda.Interpreter.Stack-sizes

-- The actual maximum stack size of the compiled program matches the
-- maximum stack size of the instrumented source-level semantics.

import Lambda.Compiler-correctness.Sizes-match

-- An example: A non-terminating program that runs in bounded stack
-- space.

import Lambda.Interpreter.Stack-sizes.Example

-- A counterexample: The trace of stack sizes produced by the virtual
-- machine is not necessarily bisimilar to that produced by the
-- instrumented interpreter.

import Lambda.Interpreter.Stack-sizes.Counterexample

-- A counterexample: The number of steps taken by the uninstrumented
-- interpreter is not, in general, linear in the number of steps taken
-- by the virtual machine for the corresponding compiled program.

import Lambda.Interpreter.Steps.Counterexample

-- A definitional interpreter that is instrumented with information
-- about the number of steps required to run the compiled program.

import Lambda.Interpreter.Steps

-- The "time complexity" of the compiled program matches the one
-- obtained from the instrumented interpreter.

import Lambda.Compiler-correctness.Steps-match