Index of /~nad/listings/definitional-interpreters

	Name	Last modified	Size	Description
	Parent Directory		-
	Accessibility.html	2023-09-29 17:41	94K
	Agda.Builtin.Bool.html	2023-09-29 17:41	3.1K
	Agda.Builtin.Char.html	2023-09-29 17:41	4.0K
	Agda.Builtin.Equalit..>	2023-09-29 17:41	2.6K
	Agda.Builtin.Float.html	2023-09-29 17:41	32K
	Agda.Builtin.Int.html	2023-09-29 17:41	3.4K
	Agda.Builtin.List.html	2023-09-29 17:41	4.7K
	Agda.Builtin.Maybe.html	2023-09-29 17:41	2.3K
	Agda.Builtin.Nat.html	2023-09-29 17:41	23K
	Agda.Builtin.Reflect..>	2023-09-29 17:41	160K
	Agda.Builtin.Sigma.html	2023-09-29 17:41	3.4K
	Agda.Builtin.Size.html	2023-09-29 17:41	4.2K
	Agda.Builtin.Strict...>	2023-09-29 17:41	4.8K
	Agda.Builtin.String...>	2023-09-29 17:41	10K
	Agda.Builtin.Unit.html	2023-09-29 17:41	1.7K
	Agda.Builtin.Word.html	2023-09-29 17:41	2.0K
	Agda.Primitive.html	2023-09-29 17:41	5.4K
	Agda.css	2023-09-29 17:41	1.8K
	Algebra.Bundles.Raw...>	2023-09-29 17:41	54K
	Algebra.Bundles.html	2023-09-29 17:41	255K
	Algebra.Consequences..>	2023-09-29 17:41	7.1K
	Algebra.Consequences..>	2023-09-29 17:41	39K
	Algebra.Consequences..>	2023-09-29 17:41	165K
	Algebra.Construct.Li..>	2023-09-29 17:41	83K
	Algebra.Construct.Na..>	2023-09-29 17:41	17K
	Algebra.Construct.Na..>	2023-09-29 17:41	7.3K
	Algebra.Construct.Na..>	2023-09-29 17:41	18K
	Algebra.Construct.Na..>	2023-09-29 17:41	13K
	Algebra.Construct.Na..>	2023-09-29 17:41	57K
	Algebra.Construct.Na..>	2023-09-29 17:41	109K
	Algebra.Core.html	2023-09-29 17:41	3.3K
	Algebra.Definitions...>	2023-09-29 17:41	16K
	Algebra.Definitions...>	2023-09-29 17:41	11K
	Algebra.Definitions...>	2023-09-29 17:41	21K
	Algebra.Definitions...>	2023-09-29 17:41	118K
	Algebra.Lattice.Bund..>	2023-09-29 17:41	7.2K
	Algebra.Lattice.Bund..>	2023-09-29 17:41	51K
	Algebra.Lattice.Cons..>	2023-09-29 17:41	4.5K
	Algebra.Lattice.Cons..>	2023-09-29 17:41	18K
	Algebra.Lattice.Cons..>	2023-09-29 17:41	6.3K
	Algebra.Lattice.Prop..>	2023-09-29 17:41	293K
	Algebra.Lattice.Prop..>	2023-09-29 17:41	6.0K
	Algebra.Lattice.Prop..>	2023-09-29 17:41	42K
	Algebra.Lattice.Prop..>	2023-09-29 17:41	11K
	Algebra.Lattice.Stru..>	2023-09-29 17:41	41K
	Algebra.Morphism.Def..>	2023-09-29 17:41	11K
	Algebra.Morphism.Str..>	2023-09-29 17:41	177K
	Algebra.Morphism.html	2023-09-29 17:41	47K
	Algebra.Properties.A..>	2023-09-29 17:41	12K
	Algebra.Properties.C..>	2023-09-29 17:41	112K
	Algebra.Properties.G..>	2023-09-29 17:41	52K
	Algebra.Properties.M..>	2023-09-29 17:41	30K
	Algebra.Properties.R..>	2023-09-29 17:41	41K
	Algebra.Properties.S..>	2023-09-29 17:41	8.2K
	Algebra.Properties.S..>	2023-09-29 17:41	38K
	Algebra.Solver.Ring...>	2023-09-29 17:41	43K
	Algebra.Solver.Ring...>	2023-09-29 17:41	96K
	Algebra.Solver.Ring...>	2023-09-29 17:41	4.3K
	Algebra.Solver.Ring...>	2023-09-29 17:41	294K
	Algebra.Structures.B..>	2023-09-29 17:41	64K
	Algebra.Structures.html	2023-09-29 17:41	210K
	Algebra.html	2023-09-29 17:41	1.9K
	Axiom.Extensionality..>	2023-09-29 17:41	21K
	Axiom.UniquenessOfId..>	2023-09-29 17:41	23K
	Bijection.html	2023-09-29 17:41	226K
	Bool.html	2023-09-29 17:41	74K
	Bounded-space.html	2023-09-29 17:41	91K
	Colist.html	2023-09-29 17:41	375K
	Conat.html	2023-09-29 17:41	432K
	Data.Bool.Base.html	2023-09-29 17:41	13K
	Data.Bool.Properties..>	2023-09-29 17:41	204K
	Data.Empty.Irrelevan..>	2023-09-29 17:41	2.2K
	Data.Empty.Polymorph..>	2023-09-29 17:41	3.8K
	Data.Empty.html	2023-09-29 17:41	4.1K
	Data.Fin.Base.html	2023-09-29 17:41	117K
	Data.Fin.Patterns.html	2023-09-29 17:41	4.3K
	Data.Fin.Properties...>	2023-09-29 17:41	540K
	Data.Irrelevant.html	2023-09-29 17:41	12K
	Data.List.Base.html	2023-09-29 17:41	194K
	Data.List.Effectful...>	2023-09-29 17:41	142K
	Data.List.Extrema.Co..>	2023-09-29 17:41	60K
	Data.List.Extrema.html	2023-09-29 17:41	132K
	Data.List.Membership..>	2023-09-29 17:41	36K
	Data.List.Membership..>	2023-09-29 17:41	202K
	Data.List.Membership..>	2023-09-29 17:41	9.3K
	Data.List.Membership..>	2023-09-29 17:41	227K
	Data.List.Membership..>	2023-09-29 17:41	19K
	Data.List.Properties..>	2023-09-29 17:41	618K
	Data.List.Relation.B..>	2023-09-29 17:41	6.3K
	Data.List.Relation.B..>	2023-09-29 17:41	48K
	Data.List.Relation.B..>	2023-09-29 17:41	26K
	Data.List.Relation.B..>	2023-09-29 17:41	37K
	Data.List.Relation.B..>	2023-09-29 17:41	127K
	Data.List.Relation.B..>	2023-09-29 17:41	2.8K
	Data.List.Relation.B..>	2023-09-29 17:41	10K
	Data.List.Relation.U..>	2023-09-29 17:41	411K
	Data.List.Relation.U..>	2023-09-29 17:41	110K
	Data.List.Relation.U..>	2023-09-29 17:41	6.3K
	Data.List.Relation.U..>	2023-09-29 17:41	36K
	Data.List.Relation.U..>	2023-09-29 17:41	452K
	Data.List.Relation.U..>	2023-09-29 17:41	38K
	Data.List.Relation.U..>	2023-09-29 17:41	5.7K
	Data.Maybe.Base.html	2023-09-29 17:41	37K
	Data.Maybe.Relation...>	2023-09-29 17:41	54K
	Data.Maybe.Relation...>	2023-09-29 17:41	31K
	Data.Nat.Base.html	2023-09-29 17:41	83K
	Data.Nat.DivMod.Core..>	2023-09-29 17:41	222K
	Data.Nat.DivMod.html	2023-09-29 17:41	363K
	Data.Nat.Divisibilit..>	2023-09-29 17:41	15K
	Data.Nat.Divisibilit..>	2023-09-29 17:41	158K
	Data.Nat.Induction.html	2023-09-29 17:41	25K
	Data.Nat.Properties...>	2023-09-29 17:41	908K
	Data.Nat.Solver.html	2023-09-29 17:41	2.4K
	Data.Nat.html	2023-09-29 17:41	5.7K
	Data.Parity.Base.html	2023-09-29 17:41	19K
	Data.Product.Algebra..>	2023-09-29 17:41	52K
	Data.Product.Base.html	2023-09-29 17:41	87K
	Data.Product.Functio..>	2023-09-29 17:41	159K
	Data.Product.Functio..>	2023-09-29 17:41	36K
	Data.Product.Functio..>	2023-09-29 17:41	55K
	Data.Product.Propert..>	2023-09-29 17:41	55K
	Data.Product.Relatio..>	2023-09-29 17:41	113K
	Data.Product.Relatio..>	2023-09-29 17:41	5.4K
	Data.Sign.Base.html	2023-09-29 17:41	8.9K
	Data.Sum.Algebra.html	2023-09-29 17:41	30K
	Data.Sum.Base.html	2023-09-29 17:41	26K
	Data.Sum.Function.Pr..>	2023-09-29 17:41	34K
	Data.Sum.Function.Se..>	2023-09-29 17:41	56K
	Data.Sum.Properties...>	2023-09-29 17:41	60K
	Data.Sum.Relation.Bi..>	2023-09-29 17:41	111K
	Data.These.Base.html	2023-09-29 17:41	36K
	Data.Unit.Base.html	2023-09-29 17:41	1.9K
	Data.Unit.Polymorphi..>	2023-09-29 17:41	3.3K
	Data.Unit.Polymorphi..>	2023-09-29 17:41	23K
	Data.Unit.Polymorphi..>	2023-09-29 17:41	1.9K
	Data.Unit.Properties..>	2023-09-29 17:41	16K
	Data.Unit.html	2023-09-29 17:41	1.7K
	Data.Vec.Base.html	2023-09-29 17:41	153K
	Data.Vec.Bounded.Bas..>	2023-09-29 17:41	68K
	Data.Vec.Functional...>	2023-09-29 17:41	69K
	Data.Vec.N-ary.html	2023-09-29 17:41	92K
	Data.Vec.html	2023-09-29 17:41	12K
	Delay-monad.Always.html	2023-09-29 17:41	14K
	Delay-monad.Bisimila..>	2023-09-29 17:41	9.0K
	Delay-monad.Bisimila..>	2023-09-29 17:41	246K
	Delay-monad.Monad.html	2023-09-29 17:41	61K
	Delay-monad.Parallel..>	2023-09-29 17:41	137K
	Delay-monad.Quantita..>	2023-09-29 17:41	426K
	Delay-monad.Sequenti..>	2023-09-29 17:41	104K
	Delay-monad.Terminat..>	2023-09-29 17:41	42K
	Delay-monad.html	2023-09-29 17:41	16K
	Double-negation.html	2023-09-29 17:41	96K
	Effect.Applicative.html	2023-09-29 17:41	36K
	Effect.Choice.html	2023-09-29 17:41	4.4K
	Effect.Empty.html	2023-09-29 17:41	3.4K
	Effect.Functor.html	2023-09-29 17:41	13K
	Effect.Monad.html	2023-09-29 17:41	32K
	Embedding.html	2023-09-29 17:41	82K
	Equality.Decidable-U..>	2023-09-29 17:41	76K
	Equality.Decision-pr..>	2023-09-29 17:41	97K
	Equality.Instances-r..>	2023-09-29 17:41	120K
	Equality.Proposition..>	2023-09-29 17:41	19K
	Equality.html	2023-09-29 17:41	1.0M
	Equivalence-relation..>	2023-09-29 17:41	82K
	Equivalence.Contract..>	2023-09-29 17:41	128K
	Equivalence.Erased.B..>	2023-09-29 17:41	97K
	Equivalence.Erased.C..>	2023-09-29 17:41	70K
	Equivalence.Half-adj..>	2023-09-29 17:41	133K
	Equivalence.List.html	2023-09-29 17:41	355K
	Equivalence.Path-spl..>	2023-09-29 17:41	413K
	Equivalence.html	2023-09-29 17:41	502K
	Erased.Basics.html	2023-09-29 17:41	14K
	Erased.Box-cong-axio..>	2023-09-29 17:41	7.0K
	Erased.Level-1.html	2023-09-29 17:41	1.0M
	Excluded-middle.html	2023-09-29 17:41	6.6K
	Extensionality.html	2023-09-29 17:41	189K
	For-iterated-equalit..>	2023-09-29 17:41	337K
	Function-universe.html	2023-09-29 17:41	2.5M
	Function.Base.html	2023-09-29 17:41	75K
	Function.Bijection.html	2023-09-29 17:41	33K
	Function.Bundles.html	2023-09-29 17:41	110K
	Function.Consequence..>	2023-09-29 17:41	22K
	Function.Consequence..>	2023-09-29 17:41	34K
	Function.Construct.C..>	2023-09-29 17:41	115K
	Function.Construct.I..>	2023-09-29 17:41	45K
	Function.Construct.S..>	2023-09-29 17:41	72K
	Function.Core.html	2023-09-29 17:41	5.0K
	Function.Definitions..>	2023-09-29 17:41	21K
	Function.Equality.html	2023-09-29 17:41	40K
	Function.Equivalence..>	2023-09-29 17:41	40K
	Function.HalfAdjoint..>	2023-09-29 17:41	46K
	Function.Injection.html	2023-09-29 17:41	23K
	Function.Inverse.html	2023-09-29 17:41	60K
	Function.LeftInverse..>	2023-09-29 17:41	42K
	Function.Metric.Bund..>	2023-09-29 17:41	37K
	Function.Metric.Core..>	2023-09-29 17:41	2.8K
	Function.Metric.Defi..>	2023-09-29 17:41	35K
	Function.Metric.Nat...>	2023-09-29 17:41	28K
	Function.Metric.Nat...>	2023-09-29 17:41	2.6K
	Function.Metric.Nat...>	2023-09-29 17:41	17K
	Function.Metric.Nat...>	2023-09-29 17:41	18K
	Function.Metric.Nat...>	2023-09-29 17:41	1.8K
	Function.Metric.Stru..>	2023-09-29 17:41	22K
	Function.Properties...>	2023-09-29 17:41	20K
	Function.Properties...>	2023-09-29 17:41	28K
	Function.Properties...>	2023-09-29 17:41	7.7K
	Function.Properties...>	2023-09-29 17:41	13K
	Function.Related.Pro..>	2023-09-29 17:41	126K
	Function.Related.Typ..>	2023-09-29 17:41	185K
	Function.Related.html	2023-09-29 17:41	163K
	Function.Structures...>	2023-09-29 17:41	43K
	Function.Surjection...>	2023-09-29 17:41	33K
	Groupoid.html	2023-09-29 17:41	189K
	H-level.Closure.html	2023-09-29 17:41	406K
	H-level.html	2023-09-29 17:41	53K
	Induction.WellFounde..>	2023-09-29 17:41	87K
	Induction.html	2023-09-29 17:41	17K
	Injection.html	2023-09-29 17:41	18K
	Integer.Basics.html	2023-09-29 17:41	40K
	Lambda.Compiler-corr..>	2023-09-29 17:41	257K
	Lambda.Compiler-corr..>	2023-09-29 17:41	241K
	Lambda.Compiler-corr..>	2023-09-29 17:41	173K
	Lambda.Compiler.html	2023-09-29 17:41	33K
	Lambda.Delay-crash-t..>	2023-09-29 17:41	100K
	Lambda.Delay-crash.html	2023-09-29 17:41	144K
	Lambda.Interpreter.S..>	2023-09-29 17:41	15K
	Lambda.Interpreter.S..>	2023-09-29 17:41	41K
	Lambda.Interpreter.S..>	2023-09-29 17:41	130K
	Lambda.Interpreter.S..>	2023-09-29 17:41	34K
	Lambda.Interpreter.S..>	2023-09-29 17:41	35K
	Lambda.Interpreter.html	2023-09-29 17:41	24K
	Lambda.Syntax.html	2023-09-29 17:41	43K
	Lambda.Type-soundnes..>	2023-09-29 17:41	52K
	Lambda.Virtual-machi..>	2023-09-29 17:41	12K
	Lambda.Virtual-machi..>	2023-09-29 17:41	36K
	Level.html	2023-09-29 17:41	5.6K
	List.html	2023-09-29 17:41	265K
	Logical-equivalence...>	2023-09-29 17:41	50K
	Maybe.html	2023-09-29 17:41	52K
	Modality.Basics.html	2023-09-29 17:41	2.1M
	Monad.Raw.html	2023-09-29 17:41	18K
	Monad.State.html	2023-09-29 17:41	37K
	Monad.html	2023-09-29 17:41	115K
	Nat.Solver.html	2023-09-29 17:41	59K
	Nat.html	2023-09-29 17:41	476K
	Omniscience.html	2023-09-29 17:41	55K
	Only-allocation.html	2023-09-29 17:41	6.9K
	Preimage.html	2023-09-29 17:41	59K
	Prelude.Size.html	2023-09-29 17:41	3.1K
	Prelude.html	2023-09-29 17:41	123K
	Pullback.html	2023-09-29 17:41	102K
	Relation.Binary.Bund..>	2023-09-29 17:41	66K
	Relation.Binary.Cons..>	2023-09-29 17:41	101K
	Relation.Binary.Cons..>	2023-09-29 17:41	72K
	Relation.Binary.Cons..>	2023-09-29 17:41	78K
	Relation.Binary.Cons..>	2023-09-29 17:41	77K
	Relation.Binary.Cons..>	2023-09-29 17:41	69K
	Relation.Binary.Cons..>	2023-09-29 17:41	83K
	Relation.Binary.Core..>	2023-09-29 17:41	19K
	Relation.Binary.Defi..>	2023-09-29 17:41	91K
	Relation.Binary.Inde..>	2023-09-29 17:41	11K
	Relation.Binary.Inde..>	2023-09-29 17:41	15K
	Relation.Binary.Inde..>	2023-09-29 17:41	13K
	Relation.Binary.Inde..>	2023-09-29 17:41	10K
	Relation.Binary.Inde..>	2023-09-29 17:41	13K
	Relation.Binary.Inde..>	2023-09-29 17:41	2.1K
	Relation.Binary.Latt..>	2023-09-29 17:41	68K
	Relation.Binary.Latt..>	2023-09-29 17:41	12K
	Relation.Binary.Latt..>	2023-09-29 17:41	61K
	Relation.Binary.Latt..>	2023-09-29 17:41	1.7K
	Relation.Binary.Morp..>	2023-09-29 17:41	6.3K
	Relation.Binary.Morp..>	2023-09-29 17:41	38K
	Relation.Binary.Prop..>	2023-09-29 17:41	15K
	Relation.Binary.Prop..>	2023-09-29 17:41	34K
	Relation.Binary.Prop..>	2023-09-29 17:41	9.8K
	Relation.Binary.Prop..>	2023-09-29 17:41	18K
	Relation.Binary.Prop..>	2023-09-29 17:41	17K
	Relation.Binary.Prop..>	2023-09-29 17:41	5.5K
	Relation.Binary.Prop..>	2023-09-29 17:41	45K
	Relation.Binary.Prop..>	2023-09-29 17:41	104K
	Relation.Binary.Prop..>	2023-09-29 17:41	53K
	Relation.Binary.Reas..>	2023-09-29 17:41	45K
	Relation.Binary.Reas..>	2023-09-29 17:41	20K
	Relation.Binary.Reas..>	2023-09-29 17:41	69K
	Relation.Binary.Reas..>	2023-09-29 17:41	3.5K
	Relation.Binary.Reas..>	2023-09-29 17:41	7.4K
	Relation.Binary.Refl..>	2023-09-29 17:41	37K
	Relation.Binary.Stru..>	2023-09-29 17:41	62K
	Relation.Binary.html	2023-09-29 17:41	1.9K
	Relation.Nullary.Dec..>	2023-09-29 17:41	56K
	Relation.Nullary.Dec..>	2023-09-29 17:41	32K
	Relation.Nullary.Ind..>	2023-09-29 17:41	3.2K
	Relation.Nullary.Neg..>	2023-09-29 17:41	21K
	Relation.Nullary.Neg..>	2023-09-29 17:41	38K
	Relation.Nullary.Ref..>	2023-09-29 17:41	34K
	Relation.Nullary.html	2023-09-29 17:41	6.5K
	Relation.Unary.Prope..>	2023-09-29 17:41	113K
	Relation.Unary.html	2023-09-29 17:41	91K
	Surjection.html	2023-09-29 17:41	88K
	TC-monad.html	2023-09-29 17:41	170K
	Tactic.By.Propositio..>	2023-09-29 17:41	121K
	Tactic.By.html	2023-09-29 17:41	145K
	Unbounded-space.html	2023-09-29 17:41	191K
	Univalence-axiom.html	2023-09-29 17:41	706K
	Upper-bounds.html	2023-09-29 17:41	299K
	Vec.Data.html	2023-09-29 17:41	39K
	Vec.Dependent.html	2023-09-29 17:41	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